OutwardConfidenceIntervals.lean

1 import KomorebiLSM.RationalConfidenceArithmetic
2 
3 /-! Exact endpoint rounding and intersection with the declared true prior. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.OutwardConfidenceIntervals
6 
7 noncomputable def roundDown (denominator : ℕ) (x : ℝ) : ℚ :=
8   (⌊(denominator : ℝ)*x⌋ : ℚ)/(denominator : ℚ)
9 noncomputable def roundUp (denominator : ℕ) (x : ℝ) : ℚ :=
10   (⌈(denominator : ℝ)*x⌉ : ℚ)/(denominator : ℚ)
11 
12 theorem roundDown_le (denominator : ℕ) (hd : 0<denominator) (x : ℝ) :
13     (roundDown denominator x : ℝ)≤x := by
14   have hdr : (0 : ℝ)<denominator := by exact_mod_cast hd
15   unfold roundDown
16   push_cast
17   apply (div_le_iff₀ hdr).mpr
18   simpa only [mul_comm] using Int.floor_le ((denominator : ℝ)*x)
19 
20 theorem le_roundUp (denominator : ℕ) (hd : 0<denominator) (x : ℝ) :
21     x≤(roundUp denominator x : ℝ) := by
22   have hdr : (0 : ℝ)<denominator := by exact_mod_cast hd
23   unfold roundUp
24   push_cast
25   apply (le_div_iff₀ hdr).mpr
26   simpa only [mul_comm] using Int.le_ceil ((denominator : ℝ)*x)
27 
28 noncomputable def lowerEndpoint (denominator : ℕ) (center : ℝ) (radius : ℚ) : ℚ :=
29   max (-1) (roundDown denominator (center-radius))
30 noncomputable def upperEndpoint (denominator : ℕ) (center : ℝ) (radius : ℚ) : ℚ :=
31   min 1 (roundUp denominator (center+radius))
32 
33 /-- Enlarging by an upper radius and rounding outward preserves every true
34 parameter that also obeys the prior interval. -/
35 theorem contains_true (denominator : ℕ) (hd : 0<denominator) (center theta bound : ℝ)
36     (radius : ℚ) (herror : |center-theta|≤bound) (hbound : bound≤(radius : ℝ))
37     (hprior : |theta|≤1) :
38     theta∈Set.Icc (lowerEndpoint denominator center radius : ℝ)
39       (upperEndpoint denominator center radius : ℝ) := by
40   have he := (abs_le.mp (herror.trans hbound))
41   have hp := abs_le.mp hprior
42   have hl := roundDown_le denominator hd (center-radius)
43   have hu := le_roundUp denominator hd (center+radius)
44   constructor
45   · unfold lowerEndpoint
46     push_cast
47     exact max_le hp.1 (by linarith)
48   · unfold upperEndpoint
49     push_cast
50     exact le_min hp.2 (by linarith)
51 
52 /-- Intersecting with a prior known to contain the truth preserves coverage,
53 including after arbitrary selection from a simultaneous event. -/
54 theorem selected_contains {Ω : Type*} (denominator : ℕ) (hd : 0<denominator)
55     (G : Set Ω) (center : ℕ → Ω → ℝ) (radius : ℕ → Ω → ℚ) (theta : ℝ)
56     (hall : ∀ ω∈G,∀ n,|center n ω-theta|≤(radius n ω : ℝ)) (hprior : |theta|≤1)
57     (time : Ω → ℕ) (ω : Ω) (hω : ω∈G) :
58     theta∈Set.Icc (lowerEndpoint denominator (center (time ω) ω) (radius (time ω) ω) : ℝ)
59       (upperEndpoint denominator (center (time ω) ω) (radius (time ω) ω) : ℝ) :=
60   contains_true denominator hd _ theta _ _ (hall ω hω (time ω)) le_rfl hprior
61 
62 end Komorebi.LSM.OutwardConfidenceIntervals

Back to source controls