SequentialConfidence.lean

1 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
2 import Mathlib.MeasureTheory.Measure.Real
3 import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
4 
5 /-! Countable, prospective confidence accounting. Conditional coverage is an
6 actual conditional expectation bound for each measurable failure event. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.SequentialConfidence
9 open MeasureTheory
10 open scoped BigOperators ENNReal NNReal
11 
12 variable {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
13 
14 /-- Conditional coverage implies unconditional coverage by total expectation. -/
15 theorem failure_bound_of_conditional {m : MeasurableSpace Ω} (hm : m≤mΩ)
16     (F : Set Ω) (hF : @MeasurableSet Ω mΩ F) (δ : NNReal)
17     (hc : ∀ᵐ ω ∂μ, (μ[F.indicator (fun _ ↦ (1:ℝ)) | m]) ω ≤ (δ:ℝ)) :
18     μ.real F ≤ (δ:ℝ) := by
19   have hi := integral_mono_ae (integrable_condExp :
20       Integrable (μ[F.indicator (fun _ ↦ (1:ℝ)) | m]) μ) (integrable_const (δ:ℝ)) hc
21   rw [integral_condExp hm] at hi
22   rw [integral_indicator hF, setIntegral_const] at hi
23   simpa using hi
24 
25 /-- A summable prospective budget controls every countably many covered stage. -/
26 theorem simultaneous_coverage (F : ℕ → Set Ω) (hF : ∀ n, MeasurableSet (F n))
27     (δn : ℕ → NNReal) (hs : Summable δn) (δ : NNReal) (hbudget : ∑' n, δn n ≤ δ)
28     (hcover : ∀ n, μ.real (F n) ≤ (δn n:ℝ)) :
29     1-(δ:ℝ) ≤ μ.real (⋂ n, (F n)ᶜ) := by
30   have hb : μ (⋃ n, F n) ≤ (δ:ENNReal) := by
31     calc
32       _ ≤ ∑' n, μ (F n) := measure_iUnion_le _
33       _ ≤ ∑' n, (δn n:ENNReal) := ENNReal.tsum_le_tsum (fun n ↦ by
34         have h := ENNReal.ofReal_le_ofReal (hcover n)
35         simpa using h)
36       _ = ↑(∑' n, δn n) := (ENNReal.coe_tsum hs).symm
37       _ ≤ _ := ENNReal.coe_le_coe.mpr hbudget
38   have hb' : μ.real (⋃ n, F n) ≤ (δ:ℝ) := by
39     have h := ENNReal.toReal_mono ENNReal.coe_ne_top hb
40     simpa only [Measure.real, ENNReal.coe_toReal] using h
41   have he : (⋂ n, (F n)ᶜ) = (⋃ n, F n)ᶜ := by simp
42   rw [he, measureReal_compl (MeasurableSet.iUnion hF)]
43   simpa using sub_le_sub_left hb' 1
44 
45 /-- P48: conditional stage coverage survives every prospective proposal sequence. -/
46 theorem conditional_simultaneous_coverage
47     (m : ℕ → MeasurableSpace Ω) (hm : ∀ n, m n≤mΩ)
48     (F : ℕ → Set Ω) (hF : ∀ n, MeasurableSet (F n))
49     (δn : ℕ → NNReal) (hs : Summable δn) (δ : NNReal) (hbudget : ∑' n, δn n ≤ δ)
50     (hc : ∀ n, ∀ᵐ ω ∂μ, (μ[(F n).indicator (fun _ ↦ (1:ℝ)) | m n]) ω ≤ (δn n:ℝ)) :
51     1-(δ:ℝ) ≤ μ.real (⋂ n, (F n)ᶜ) :=
52   simultaneous_coverage F hF δn hs δ hbudget
53     (fun n ↦ failure_bound_of_conditional (hm n) (F n) (hF n) (δn n) (hc n))
54 
55 /-- P48's robust acceptance conclusion on one event of confidence at least 1−δ.
56 The covered initial base and exact robust implication remain explicit. -/
57 theorem conditional_robust_certificate {Θ D : Type*}
58     (m : ℕ → MeasurableSpace Ω) (hm : ∀ n, m n≤mΩ)
59     (trueModel : ℕ → Ω → Θ) (U : ℕ → Ω → Set Θ)
60     (hF : ∀ n, MeasurableSet {ω | trueModel n ω ∉ U n ω})
61     (δn : ℕ → NNReal) (hs : Summable δn) (δ : NNReal) (hbudget : ∑' n, δn n ≤ δ)
62     (hc : ∀ n, ∀ᵐ ω ∂μ,
63       (μ[({ω | trueModel n ω ∉ U n ω}).indicator (fun _ ↦ (1:ℝ)) | m n]) ω ≤ (δn n:ℝ))
64     (domain : ℕ → Ω → D) (Accepted InitialCovered : ℕ → Ω → Prop)
65     (Valid : Θ → D → Prop)
66     (sound : ∀ n ω θ, Accepted n ω → InitialCovered n ω → θ ∈ U n ω →
67       Valid θ (domain n ω)) :
68     1-(δ:ℝ) ≤ μ.real {ω | ∀ n, Accepted n ω → InitialCovered n ω →
69       Valid (trueModel n ω) (domain n ω)} := by
70   have hprob := conditional_simultaneous_coverage m hm
71     (fun n ↦ {ω | trueModel n ω ∉ U n ω}) hF δn hs δ hbudget hc
72   apply hprob.trans (measureReal_mono ?_)
73   intro ω hω
74   change ∀ n, Accepted n ω → InitialCovered n ω → Valid (trueModel n ω) (domain n ω)
75   intro n ha hi
76   have hcover : trueModel n ω ∈ U n ω := by
77     have hn := Set.mem_iInter.mp hω n
78     simpa using hn
79   exact sound n ω (trueModel n ω) ha hi hcover
80 
81 omit mΩ in
82 /-- An arbitrary selected stage is among the simultaneously valid stages.
83 In particular this applies to every stopping time defined from recorded data. -/
84 theorem validity_at_selected_stage {Θ D : Type*}
85     (trueModel : ℕ → Ω → Θ) (domain : ℕ → Ω → D)
86     (Accepted InitialCovered : ℕ → Ω → Prop) (Valid : Θ → D → Prop)
87     (ω : Ω) (hall : ∀ n, Accepted n ω → InitialCovered n ω →
88       Valid (trueModel n ω) (domain n ω))
89     (selected : Ω → ℕ) (ha : Accepted (selected ω) ω)
90     (hi : InitialCovered (selected ω) ω) :
91     Valid (trueModel (selected ω) ω) (domain (selected ω) ω) :=
92   hall (selected ω) ha hi
93 
94 end Komorebi.LSM.SequentialConfidence

Back to source controls