PredictableResidualAnytime.lean

1 import KomorebiLSM.PredictableResidualGeneral
2 
3 /-! The actual all-time union bound on arbitrary sample spaces and arbitrary
4 finite/countable prospectively registered rule indices, with unchanged budgets. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.PredictableResidualGeneral
7 open MeasureTheory ProbabilityTheory Real PredictableResidual
8 open scoped BigOperators NNReal ENNReal
9 variable {Ω : Type*} [mΩ : MeasurableSpace Ω]
10 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
11 
12 /-- One predictable rule has the declared simultaneous boundary at every positive time. -/
13 theorem time_uniform_one (ℱ : Filtration ℕ mΩ) (X : ℕ → Ω → ℝ)
14     (hX : ∀ i, Measurable[ℱ (i+1)] (X i))
15     (hb : ∀ i, ∀ᵐ ω ∂μ, X i ω∈Set.Icc (0:ℝ) 1)
16     (α : NNReal) (hα : 0<α) (hα1 : α≤1) :
17     1-(α:ℝ) ≤ μ.real {ω | ∀ n, |centeredSum (μ:=μ) ℱ X (n+1) ω|≤boundary (n+1) α} := by
18   let F : ℕ → Set Ω := fun n ↦ {ω | boundary (n+1) α < |centeredSum (μ:=μ) ℱ X (n+1) ω|}
19   have hF : ∀ n, MeasurableSet (F n) := by
20     intro n
21     apply measurableSet_lt measurable_const
22     exact (centeredSum_measurable ℱ X hX (n+1)).norm
23   have hweights : Summable (fun n ↦ α*timeWeight n) := time_summable.mul_left α
24   have hbudget : ∑' n, α*timeWeight n ≤ α := by
25     rw [tsum_mul_left]
26     simpa using mul_le_mul_of_nonneg_left time_budget α.coe_nonneg
27   have hf : ∀ n, μ.real (F n) ≤ (α*timeWeight n:NNReal) := by
28     intro n
29     have ht := predictable_sum_tail ℱ X hX hb (by omega : 0<n+1)
30       (boundary (n+1) α) (sqrt_nonneg _)
31     rw [boundary_budget (by omega) (by exact_mod_cast hα) (by exact_mod_cast hα1)] at ht
32     apply (measureReal_mono (by
33       intro ω h
34       exact (show boundary (n+1) α < |centeredSum (μ:=μ) ℱ X (n+1) ω| from h).le)).trans
35       (ht.trans_eq ?_)
36     simp only [timeWeight,NNReal.coe_mul,NNReal.coe_div,NNReal.coe_one,NNReal.coe_add,NNReal.coe_natCast]
37     push_cast
38     field_simp
39     ring
40   have hprob := CountableConfidence.simultaneous_coverage F hF
41     (fun n ↦ α*timeWeight n) hweights α hbudget hf
42   convert hprob using 1
43   congr 1
44   ext ω
45   simp [F]
46 
47 variable {J : Type*} [Countable J]
48 
49 /-- All prospectively registered countably many rules share one all-time event. -/
50 theorem time_uniform_rules (ℱ : Filtration ℕ mΩ) (X : J → ℕ → Ω → ℝ)
51     (hX : ∀ j i, Measurable[ℱ (i+1)] (X j i))
52     (hb : ∀ j i, ∀ᵐ ω ∂μ, X j i ω∈Set.Icc (0:ℝ) 1)
53     (α : J → NNReal) (hα : ∀ j, 0<α j) (hs : Summable α)
54     (δ : NNReal) (hbudget : ∑' j, α j ≤ δ) (hδ1 : δ≤1) :
55     1-(δ:ℝ) ≤ μ.real {ω | ∀ j n,
56       |centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤boundary (n+1) (α j)} := by
57   let F : J → Set Ω := fun j ↦ {ω | ∃ n,
58     boundary (n+1) (α j) < |centeredSum (μ:=μ) ℱ (X j) (n+1) ω|}
59   have hF : ∀ j, MeasurableSet (F j) := by
60     intro j
61     simp only [F,Set.ofPred_exists]
62     apply MeasurableSet.iUnion
63     intro n
64     apply measurableSet_lt measurable_const
65     exact (centeredSum_measurable ℱ (X j) (hX j) (n+1)).norm
66   have hf : ∀ j, μ.real (F j)≤(α j:ℝ) := by
67     intro j
68     have hj : α j≤1 := (hs.le_tsum j (fun _ _ ↦ by positivity)).trans (hbudget.trans hδ1)
69     have ht := time_uniform_one ℱ (X j) (hX j) (hb j) (α j) (hα j) hj
70     have he : {ω | ∀ n, |centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤boundary (n+1) (α j)} =
71         (F j)ᶜ := by ext ω; simp [F]
72     rw [he,measureReal_compl (hF j)] at ht
73     simp only [probReal_univ] at ht
74     linarith
75   have hprob := CountableConfidence.simultaneous_coverage F hF α hs δ hbudget hf
76   convert hprob using 1
77   congr 1
78   ext ω
79   simp [F]
80 
81 
82 omit [IsProbabilityMeasure μ] in
83 /-- The simultaneous unit-range event is genuinely measurable. -/
84 theorem unit_event_measurable (ℱ : Filtration ℕ mΩ) (X : J → ℕ → Ω → ℝ)
85     (hX : ∀ j i,Measurable[ℱ (i+1)] (X j i)) (α : J → NNReal) :
86     MeasurableSet {ω | ∀ j n,|centeredSum (μ:=μ) ℱ (X j) (n+1) ω|≤boundary (n+1) (α j)} := by
87   simp only [Set.ofPred_forall]
88   apply MeasurableSet.iInter
89   intro j
90   apply MeasurableSet.iInter
91   intro n
92   exact measurableSet_le (centeredSum_measurable ℱ (X j) (hX j) (n+1)).norm measurable_const
93 
94 end Komorebi.LSM.PredictableResidualGeneral

Back to source controls