Lineage.lean

1 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
2 import Mathlib.MeasureTheory.Measure.Real
3 import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
4 
5 /-! # Conditional error budgets across an adaptive lineage
6 
7 Core 7.4 on an arbitrary probability space. `H j` is the information available
8 before the source's attempt `j + 1`. Each assumption concerns the false-acceptance
9 event of that actual attempt, after its history-dependent candidate choice.
10 
11 No independence, finite sample space, or monotonicity of `H` is needed for this
12 consequence. The conditional premise itself must be justified by the application.
13 A numerical schedule, or marginal bounds for candidates fixed in advance, does
14 not establish it. Real budget sums carry an explicit summability hypothesis.
15 -/
16 namespace Komorebi.MachineTheory.Lineage
17 
18 open MeasureTheory Set Filter
19 open scoped ENNReal NNReal Topology
20 noncomputable section
21 
22 variable {Ω : Type*} [mΩ : MeasurableSpace Ω]
23 
24 /-- The actual conditional expectation of the false-event indicator. -/
25 def conditionalRisk (μ : Measure Ω) (H : MeasurableSpace Ω) (A : Set Ω) : Ω → ℝ :=
26   μ[A.indicator (fun _ => (1 : ℝ)) | H]
27 
28 /-- Conditional validity for one actual attempt, with a deterministic budget. -/
29 def ConditionalBound (μ : Measure Ω) (H : MeasurableSpace Ω)
30     (A : Set Ω) (d : ℝ) : Prop := by
31   letI : MeasurableSpace Ω := mΩ
32   exact ∀ᵐ ω ∂μ, conditionalRisk μ H A ω ≤ d
33 
34 variable (μ : Measure Ω) [IsProbabilityMeasure μ]
35 
36 /-- The indicator is genuinely integrable, so its integral is a probability. -/
37 theorem indicator_integrable (A : Set Ω) (hA : MeasurableSet A) :
38     Integrable (A.indicator (fun _ => (1 : ℝ))) μ :=
39   (integrable_const (1 : ℝ)).indicator hA
40 
41 /-- Taking expectations here uses Mathlib's conditional expectation integral law. -/
42 theorem conditional_integral_eq_probability (H : MeasurableSpace Ω) (hH : H ≤ mΩ)
43     (A : Set Ω) (hA : MeasurableSet[mΩ] A) :
44     (letI : MeasurableSpace Ω := mΩ
45      (∫ ω, conditionalRisk μ H A ω ∂μ) = μ.real A) := by
46   let : MeasurableSpace Ω := mΩ
47   unfold conditionalRisk
48   rw [integral_condExp hH, integral_indicator_const (1 : ℝ) hA]
49   simp
50 
51 /-- Conditional validity of the actual event implies its marginal bound. -/
52 theorem conditional_marginal_bound (H : MeasurableSpace Ω) (hH : H ≤ mΩ)
53     (A : Set Ω) (hA : MeasurableSet[mΩ] A) (d : ℝ)
54     (h : ConditionalBound (mΩ := mΩ) μ H A d) : μ.real A ≤ d := by
55   let : MeasurableSpace Ω := mΩ
56   calc
57     μ.real A = ∫ ω, conditionalRisk μ H A ω ∂μ :=
58       (conditional_integral_eq_probability μ H hH A hA).symm
59     _ ≤ ∫ _ : Ω, d ∂μ :=
60       integral_mono_ae integrable_condExp (integrable_const d) h
61     _ = d := by simp
62 
63 /-- A real probability bound transports to the extended nonnegative measure. -/
64 theorem measure_le_of_real_bound (A : Set Ω) (d : ℝ) (h : μ.real A ≤ d) :
65     μ A ≤ ENNReal.ofReal d := by
66   have hp := ENNReal.ofReal_le_ofReal h
67   simpa only [measureReal_def, ENNReal.ofReal_toReal (measure_ne_top μ A)] using hp
68 
69 omit [IsProbabilityMeasure μ] in
70 /-- The finite union bound uses the budgets of precisely the selected attempts. -/
71 theorem finite_union_bound_of_marginals (A : ℕ → Set Ω) (d : ℕ → ℝ)
72     (h : ∀ j, μ.real (A j) ≤ d j) (s : Finset ℕ) :
73     μ.real (⋃ j ∈ s, A j) ≤ ∑ j ∈ s, d j := by
74   exact (measureReal_biUnion_finset_le s A).trans (Finset.sum_le_sum fun j _ => h j)
75 
76 /-- Countable subadditivity in `ℝ≥0∞`; this step has no real-tsum convention. -/
77 theorem countable_union_ennreal_bound_of_marginals (A : ℕ → Set Ω) (d : ℕ → ℝ)
78     (h : ∀ j, μ.real (A j) ≤ d j) :
79     μ (⋃ j, A j) ≤ ∑' j, ENNReal.ofReal (d j) := by
80   exact (measure_iUnion_le A).trans
81     (ENNReal.tsum_le_tsum fun j => measure_le_of_real_bound μ (A j) (d j) (h j))
82 
83 /-- Summability makes the real total faithful to the extended nonnegative sum. -/
84 theorem countable_union_bound_of_marginals (A : ℕ → Set Ω) (d : ℕ → ℝ)
85     (hd : ∀ j, 0 ≤ d j) (hs : Summable d)
86     (h : ∀ j, μ.real (A j) ≤ d j) :
87     μ.real (⋃ j, A j) ≤ ∑' j, d j := by
88   have he := countable_union_ennreal_bound_of_marginals μ A d h
89   rw [← ENNReal.ofReal_tsum_of_nonneg hd hs] at he
90   have hr := ENNReal.toReal_mono ENNReal.ofReal_ne_top he
91   simpa only [← measureReal_def, ENNReal.toReal_ofReal (tsum_nonneg hd)] using hr
92 
93 /-- Core 7.4, finite-attempt conclusion from the actual conditional premises. -/
94 theorem finite_lineage_bound (H : ℕ → MeasurableSpace Ω) (hH : ∀ j, H j ≤ mΩ)
95     (A : ℕ → Set Ω) (hA : ∀ j, MeasurableSet (A j)) (d : ℕ → ℝ)
96     (hc : ∀ j, ConditionalBound μ (H j) (A j) (d j)) (s : Finset ℕ) :
97     μ.real (⋃ j ∈ s, A j) ≤ ∑ j ∈ s, d j := by
98   exact finite_union_bound_of_marginals μ A d
99     (fun j => conditional_marginal_bound μ (H j) (hH j) (A j) (hA j) (d j) (hc j)) s
100 
101 /-- Core 7.4, countably many actual attempts with a deterministic total budget. -/
102 theorem lineage_bound (H : ℕ → MeasurableSpace Ω) (hH : ∀ j, H j ≤ mΩ)
103     (A : ℕ → Set Ω) (hA : ∀ j, MeasurableSet (A j)) (d : ℕ → ℝ)
104     (hd : ∀ j, 0 ≤ d j) (hs : Summable d) (total : ℝ)
105     (htotal : (∑' j, d j) ≤ total)
106     (hc : ∀ j, ConditionalBound μ (H j) (A j) (d j)) :
107     μ.real (⋃ j, A j) ≤ total := by
108   exact (countable_union_bound_of_marginals μ A d hd hs
109     (fun j => conditional_marginal_bound μ (H j) (hH j) (A j) (hA j) (d j) (hc j))).trans htotal
110 
111 /-- The corresponding nontruncated, extended-measure conclusion. -/
112 theorem lineage_ennreal_bound (H : ℕ → MeasurableSpace Ω) (hH : ∀ j, H j ≤ mΩ)
113     (A : ℕ → Set Ω) (hA : ∀ j, MeasurableSet (A j)) (d : ℕ → ℝ)
114     (hd : ∀ j, 0 ≤ d j) (hs : Summable d) (total : ℝ)
115     (htotal : (∑' j, d j) ≤ total)
116     (hc : ∀ j, ConditionalBound μ (H j) (A j) (d j)) :
117     μ (⋃ j, A j) ≤ ENNReal.ofReal total :=
118   measure_le_of_real_bound μ _ _ (lineage_bound μ H hH A hA d hd hs total htotal hc)
119 
120 /-- A history-dependent gate only removes outcomes from each attempt's event. -/
121 def gatedEvents (A gate : ℕ → Set Ω) (j : ℕ) : Set Ω := A j ∩ gate j
122 
123 omit mΩ in
124 /-- Containment is pointwise and does not require independence or predictable gates. -/
125 theorem gated_union_subset (A gate : ℕ → Set Ω) :
126     (⋃ j, gatedEvents A gate j) ⊆ ⋃ j, A j := by
127   intro ω hω
128   obtain ⟨j,hj⟩ := mem_iUnion.mp hω
129   exact mem_iUnion.mpr ⟨j,hj.1⟩
130 
131 /-- Measurable gates give genuine measurable false-acceptance events. -/
132 theorem gatedEvents_measurable (A gate : ℕ → Set Ω)
133     (hA : ∀ j, MeasurableSet (A j)) (hg : ∀ j, MeasurableSet (gate j)) (j : ℕ) :
134     MeasurableSet (gatedEvents A gate j) := (hA j).inter (hg j)
135 
136 /-- Even arbitrary gates cannot enlarge the outer measure of ever failing. -/
137 theorem gated_lineage_bound (H : ℕ → MeasurableSpace Ω) (hH : ∀ j, H j ≤ mΩ)
138     (A : ℕ → Set Ω) (hA : ∀ j, MeasurableSet (A j)) (d : ℕ → ℝ)
139     (hd : ∀ j, 0 ≤ d j) (hs : Summable d) (total : ℝ)
140     (htotal : (∑' j, d j) ≤ total)
141     (hc : ∀ j, ConditionalBound μ (H j) (A j) (d j)) (gate : ℕ → Set Ω) :
142     μ.real (⋃ j, gatedEvents A gate j) ≤ total :=
143   (measureReal_mono (gated_union_subset A gate)).trans
144     (lineage_bound μ H hH A hA d hd hs total htotal hc)
145 
146 /-- `stop ω` is the number of attempted indices, possibly infinite. -/
147 def stoppedEvents (A : ℕ → Set Ω) (stop : Ω → WithTop ℕ) (j : ℕ) : Set Ω :=
148   gatedEvents A (fun k => {ω | (k : WithTop ℕ) < stop ω}) j
149 
150 omit mΩ in
151 /-- Arbitrary outcome-dependent stopping only removes potential false acceptances. -/
152 theorem stopped_union_subset (A : ℕ → Set Ω) (stop : Ω → WithTop ℕ) :
153     (⋃ j, stoppedEvents A stop j) ⊆ ⋃ j, A j :=
154   gated_union_subset A _
155 
156 /-- Core 7.4 with stopping. A stopping-time law is unnecessary for containment. -/
157 theorem stopped_lineage_bound (H : ℕ → MeasurableSpace Ω) (hH : ∀ j, H j ≤ mΩ)
158     (A : ℕ → Set Ω) (hA : ∀ j, MeasurableSet (A j)) (d : ℕ → ℝ)
159     (hd : ∀ j, 0 ≤ d j) (hs : Summable d) (total : ℝ)
160     (htotal : (∑' j, d j) ≤ total)
161     (hc : ∀ j, ConditionalBound μ (H j) (A j) (d j)) (stop : Ω → WithTop ℕ) :
162     μ.real (⋃ j, stoppedEvents A stop j) ≤ total :=
163   gated_lineage_bound μ H hH A hA d hd hs total htotal hc _
164 
165 /-- The source's actual event includes the candidate chosen on this outcome. -/
166 def selectedFalseEvents {Candidate : Type*} (selected : ℕ → Ω → Candidate)
167     (accepted : ℕ → Ω → Prop) (falseClaim : Candidate → Ω → Prop) (j : ℕ) : Set Ω :=
168   {ω | accepted j ω ∧ falseClaim (selected j ω) ω}
169 
170 /-- A candidate-selection wrapper keeps the conditional premise on the actual event. -/
171 theorem selected_lineage_bound {Candidate : Type*}
172     (selected : ℕ → Ω → Candidate) (accepted : ℕ → Ω → Prop)
173     (falseClaim : Candidate → Ω → Prop)
174     (H : ℕ → MeasurableSpace Ω) (hH : ∀ j, H j ≤ mΩ)
175     (hA : ∀ j, MeasurableSet (selectedFalseEvents selected accepted falseClaim j))
176     (d : ℕ → ℝ) (hd : ∀ j, 0 ≤ d j) (hs : Summable d) (total : ℝ)
177     (htotal : (∑' j, d j) ≤ total)
178     (hc : ∀ j, ConditionalBound μ (H j)
179       (selectedFalseEvents selected accepted falseClaim j) (d j)) :
180     μ.real (⋃ j, selectedFalseEvents selected accepted falseClaim j) ≤ total :=
181   lineage_bound μ H hH _ hA d hd hs total htotal hc
182 
183 /-- The same actual selected events may be restricted by outcome-dependent stopping. -/
184 theorem stopped_selected_lineage_bound {Candidate : Type*}
185     (selected : ℕ → Ω → Candidate) (accepted : ℕ → Ω → Prop)
186     (falseClaim : Candidate → Ω → Prop)
187     (H : ℕ → MeasurableSpace Ω) (hH : ∀ j, H j ≤ mΩ)
188     (hA : ∀ j, MeasurableSet (selectedFalseEvents selected accepted falseClaim j))
189     (d : ℕ → ℝ) (hd : ∀ j, 0 ≤ d j) (hs : Summable d) (total : ℝ)
190     (htotal : (∑' j, d j) ≤ total)
191     (hc : ∀ j, ConditionalBound μ (H j)
192       (selectedFalseEvents selected accepted falseClaim j) (d j))
193     (stop : Ω → WithTop ℕ) :
194     μ.real (⋃ j, stoppedEvents (selectedFalseEvents selected accepted falseClaim) stop j) ≤ total :=
195   stopped_lineage_bound μ H hH _ hA d hd hs total htotal hc stop
196 
197 /-- Measurable continuation events give measurable stopped false-acceptance events. -/
198 theorem stoppedEvents_measurable (A : ℕ → Set Ω) (stop : Ω → WithTop ℕ)
199     (hA : ∀ j, MeasurableSet (A j))
200     (hstop : ∀ j : ℕ, MeasurableSet {ω | (j : WithTop ℕ) < stop ω}) (j : ℕ) :
201     MeasurableSet (stoppedEvents A stop j) := gatedEvents_measurable A _ hA hstop j
202 
203 /-- A constant positive real schedule is not summable. -/
204 theorem constant_one_not_summable : ¬ Summable (fun _ : ℕ => (1 : ℝ)) := by
205   rw [summable_const_iff]
206   exact one_ne_zero
207 
208 /-- Lean's real total defaults to zero on this divergent schedule. -/
209 theorem divergent_real_tsum_zero : (∑' _ : ℕ, (1 : ℝ)) = 0 :=
210   tsum_eq_zero_of_not_summable constant_one_not_summable
211 
212 /-- The extended nonnegative sum correctly records infinite total expenditure. -/
213 theorem divergent_ennreal_tsum_top : (∑' _ : ℕ, (1 : ℝ≥0∞)) = ⊤ :=
214   ENNReal.tsum_const_eq_top_of_ne_zero one_ne_zero
215 
216 /-- The divergent real convention cannot bound a sequence of certain failures. -/
217 theorem divergent_real_total_not_union_bound :
218     ¬ μ.real (⋃ _ : ℕ, (Set.univ : Set Ω)) ≤ ∑' _ : ℕ, (1 : ℝ) := by
219   rw [divergent_real_tsum_zero]
220   simp only [Set.iUnion_const, measureReal_def, measure_univ, ENNReal.toReal_one]
221   norm_num
222 
223 end
224 end Komorebi.MachineTheory.Lineage

Back to source controls