CountableConfidence.lean

1 import KomorebiLSM.SequentialConfidence
2 
3 /-! Exact prospective confidence accounting for arbitrary finite/countable
4 rule indices. Reindexing changes neither the events nor their total budget. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.CountableConfidence
7 open MeasureTheory
8 open scoped BigOperators ENNReal NNReal
9 variable {Ω J : Type*} [MeasurableSpace Ω] [Countable J]
10 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
11 
12 /-- The actual countable union bound, with the original total budget. -/
13 theorem simultaneous_coverage (F : J → Set Ω) (hF : ∀ j,MeasurableSet (F j))
14     (α : J → NNReal) (hs : Summable α) (δ : NNReal) (hbudget : ∑' j,α j≤δ)
15     (hcover : ∀ j,μ.real (F j)≤(α j:ℝ)) :
16     1-(δ:ℝ)≤μ.real (⋂ j,(F j)ᶜ) := by
17   have hb : μ (⋃ j,F j)≤(δ:ENNReal) := by
18     calc
19       _ ≤ ∑' j,μ (F j) := measure_iUnion_le _
20       _ ≤ ∑' j,(α j:ENNReal) := ENNReal.tsum_le_tsum (fun j => by
21         have h := ENNReal.ofReal_le_ofReal (hcover j)
22         simpa using h)
23       _ = ↑(∑' j,α j) := (ENNReal.coe_tsum hs).symm
24       _ ≤ _ := ENNReal.coe_le_coe.mpr hbudget
25   have hb' : μ.real (⋃ j,F j)≤(δ:ℝ) := by
26     have h := ENNReal.toReal_mono ENNReal.coe_ne_top hb
27     simpa only [Measure.real,ENNReal.coe_toReal] using h
28   have he : (⋂ j,(F j)ᶜ)=(⋃ j,F j)ᶜ := by simp
29   rw [he,measureReal_compl (MeasurableSet.iUnion hF)]
30   simpa using sub_le_sub_left hb' 1
31 
32 omit [MeasurableSpace Ω] [Countable J] in
33 /-- An equivalence preserves summability and the actual total budget exactly. -/
34 theorem budget_transport {K : Type*} (e : K ≃ J) (α : J → NNReal) (hs : Summable α) :
35     Summable (fun k => α (e k)) ∧ (∑' k,α (e k))=∑' j,α j := by
36   exact ⟨e.summable_iff.mpr hs,e.tsum_eq α⟩
37 
38 omit [MeasurableSpace Ω] [Countable J] in
39 /-- Relabeling rules changes no simultaneous pathwise assertion. -/
40 theorem forall_transport {K : Type*} (e : K ≃ J) (P : J → Prop) :
41     (∀ k,P (e k)) ↔ ∀ j,P j := by
42   constructor
43   · intro h j
44     simpa using h (e.symm j)
45   · exact fun h k => h (e k)
46 
47 /-- Finite-family accounting uses the literal finite sum, without padded rules. -/
48 theorem finite_simultaneous_coverage [Fintype J]
49     (F : J → Set Ω) (hF : ∀ j,MeasurableSet (F j))
50     (α : J → NNReal) (δ : NNReal) (hbudget : ∑ j,α j≤δ)
51     (hcover : ∀ j,μ.real (F j)≤(α j:ℝ)) :
52     1-(δ:ℝ)≤μ.real (⋂ j,(F j)ᶜ) := by
53   apply simultaneous_coverage F hF α (summable_of_hasFiniteSupport (Set.toFinite _)) δ
54   · simpa only [tsum_fintype] using hbudget
55   · exact hcover
56 
57 end Komorebi.LSM.CountableConfidence

Back to source controls