PositiveCellApproximation.lean

1 import KomorebiLSM.ContinuousBins
2 import KomorebiLSM.BaseNormIntegration
3 import KomorebiLSM.CellDistance
4 import Mathlib.MeasureTheory.Integral.Prod
5 
6 /-! P58: positive approximations are literal normalized Bochner cell averages.
7 The approximation, its exact event operators, and its resolution error all use
8 one actual reference measure and the positive-decomposition base norm. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.PositiveCellApproximation
11 open MeasureTheory ContinuousInstrument ContinuousBins
12 open scoped BigOperators
13 variable {E A Y I : Type*} [MeasurableSpace Y] [Fintype I]
14 
15 /-- A finite partition modulo a reference null set, with positive cell masses.
16 This includes literal partitions and interval partitions of a supported measure. -/
17 structure CellPartition (μ : Measure Y) (I : Type*) [Fintype I] where
18   cell : I → Set Y
19   measurable : ∀ i,MeasurableSet (cell i)
20   disjoint : Pairwise (fun i j => Disjoint (cell i) (cell j))
21   cover : ∀ᵐ y∂μ,∃ i,y∈cell i
22   mass_positive : ∀ i,0<μ.real (cell i)
23 
24 namespace CellPartition
25 variable {μ : Measure Y} (P : CellPartition μ I)
26 
27 theorem restrict_union : μ.restrict (⋃ i,P.cell i)=μ :=
28   Measure.restrict_eq_self_of_ae_mem (by simpa only [Set.mem_iUnion] using P.cover)
29 
30 theorem total_mass [IsProbabilityMeasure μ] : ∑ i,μ.real (P.cell i)=1 := by
31   rw [← measureReal_iUnion_fintype P.disjoint P.measurable]
32   have h := congrArg (fun ν : Measure Y => ν.real Set.univ) P.restrict_union
33   simpa using h
34 
35 theorem integral_partition {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
36     (f : Y → F) (hf : Integrable f μ) :
37     (∫ y,f y∂μ)=∑ i,∫ y in P.cell i,f y∂μ := by
38   rw [← integral_iUnion_fintype P.measurable P.disjoint (fun _ => hf.integrableOn),P.restrict_union]
39 
40 end CellPartition
41 
42 variable [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
43 variable [MeasurableSpace E] [BorelSpace E]
44 variable {C : BaseNorm.ProbabilityCone E} {μ : Measure Y} [IsProbabilityMeasure μ]
45 /-- The induced norm is the actual supremum over the unit ball of the
46 positive-decomposition base norm. -/
47 noncomputable def inducedNorm (T : E →L[ℝ] E) : ℝ :=
48   sSup {r | ∃ z : E,C.value z≤1 ∧ r=C.value (T z)}
49 
50 omit [MeasurableSpace E] [BorelSpace E] in
51 theorem inducedNorm_bdd (T : E →L[ℝ] E) :
52     BddAbove {r | ∃ z : E,C.value z≤1 ∧ r=C.value (T z)} := by
53   obtain ⟨K,hK,hKv⟩ := C.value_le_const_mul_norm
54   obtain ⟨R,hR,hRv⟩ := C.exists_norm_le_value
55   refine ⟨K*(‖T‖*R),?_⟩
56   rintro r ⟨z,hz,rfl⟩
57   calc
58     C.value (T z) ≤ K*‖T z‖ := hKv _
59     _ ≤ K*(‖T‖*‖z‖) := mul_le_mul_of_nonneg_left (T.le_opNorm z) hK.le
60     _ ≤ K*(‖T‖*(R*C.value z)) :=
61       mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left (hRv z) (norm_nonneg T)) hK.le
62     _ ≤ K*(‖T‖*(R*1)) :=
63       mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_left
64         (mul_le_mul_of_nonneg_left hz hR.le) (norm_nonneg T)) hK.le
65     _ = _ := by rw [mul_one]
66 
67 omit [MeasurableSpace E] [BorelSpace E] in
68 theorem inducedNorm_nonneg (T : E →L[ℝ] E) : 0≤ inducedNorm (C := C) T := by
69   apply le_csSup (inducedNorm_bdd T)
70   exact ⟨0,by simp,by simp⟩
71 
72 omit [MeasurableSpace E] [BorelSpace E] in
73 /-- The supremum genuinely controls every input by homogeneity. -/
74 theorem value_apply_le_inducedNorm (T : E →L[ℝ] E) (z : E) :
75     C.value (T z)≤ inducedNorm (C := C) T*C.value z := by
76   by_cases hz : z=0
77   · simp [hz]
78   have hp : 0<C.value z := lt_of_le_of_ne (C.value_nonneg z)
79     (Ne.symm (fun h => hz ((C.value_eq_zero_iff z).mp h)))
80   let x := (C.value z)⁻¹ • z
81   have hx : C.value x≤1 := by
82     change C.value ((C.value z)⁻¹ • z)≤1
83     rw [C.value_smul_of_nonneg (inv_nonneg.mpr hp.le),inv_mul_cancel₀ hp.ne']
84   have hb : C.value (T x)≤ inducedNorm (C := C) T :=
85     le_csSup (inducedNorm_bdd T) ⟨x,hx,rfl⟩
86   have he : z=C.value z • x := by simp [x,smul_smul,hp.ne']
87   calc
88     C.value (T z)=C.value z*C.value (T x) := by
89       conv_lhs => rw [he,map_smul,C.value_smul_of_nonneg hp.le]
90     _ ≤ C.value z*inducedNorm (C := C) T := mul_le_mul_of_nonneg_left hb hp.le
91     _ = _ := mul_comm _ _
92 
93 variable (D : DensityInstrument (A := A) C μ) (P : CellPartition μ I)
94 
95 /-- Normalization is by the positive reference mass of the actual cell. -/
96 noncomputable def cellAverage (a : A) (i : I) : E →L[ℝ] E :=
97   (μ.real (P.cell i))⁻¹ • cellOperator μ (D.op a) (P.cell i)
98 
99 /-- The lifted density is constant on each cell and zero on the exceptional
100 uncovered null set. No representative point is substituted for the integral. -/
101 noncomputable def operator (a : A) (y : Y) : E →L[ℝ] E :=
102   ∑ i,(P.cell i).indicator (fun _ => cellAverage D P a i) y
103 
104 omit [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [IsProbabilityMeasure μ] in
105 theorem operator_on_cell (a : A) (i : I) {y : Y} (hy : y∈P.cell i) :
106     operator D P a y=cellAverage D P a i := by
107   classical
108   unfold operator
109   rw [Finset.sum_eq_single i]
110   · exact Set.indicator_of_mem hy _
111   · intro j _ hji
112     have hj : y∉P.cell j := fun hj => Set.disjoint_left.mp (P.disjoint hji) hj hy
113     exact Set.indicator_of_notMem hj _
114   · simp
115 
116 omit [MeasurableSpace E] [BorelSpace E] in
117 theorem cellAverage_positive (a : A) (i : I) {z : E} (hz : z∈C.carrier) :
118     cellAverage D P a i z∈C.carrier :=
119   C.smul_mem (inv_nonneg.mpr (P.mass_positive i).le)
120     (cellOperator_positive C μ (D.op a) (D.integrable_op a) (D.positive a)
121       (P.cell i) (P.measurable i) z hz)
122 
123 omit [MeasurableSpace E] [BorelSpace E] in
124 theorem operator_positive (a : A) (y : Y) {z : E} (hz : z∈C.carrier) :
125     operator D P a y z∈C.carrier := by
126   classical
127   by_cases hy : ∃ i,y∈P.cell i
128   · obtain ⟨i,hi⟩ := hy
129     rw [operator_on_cell D P a i hi]
130     exact cellAverage_positive D P a i hz
131   · have ho : operator D P a y=0 := by
132       apply Finset.sum_eq_zero
133       intro i _
134       exact Set.indicator_of_notMem (fun hi => hy ⟨i,hi⟩) _
135     rw [ho]
136     exact C.zero_mem
137 
138 omit [MeasurableSpace E] [BorelSpace E] [IsProbabilityMeasure μ] in
139 theorem operator_measurable (a : A) : Measurable (operator D P a) :=
140   Finset.measurable_fun_sum _ (fun i _ => measurable_const.indicator (P.measurable i))
141 
142 omit [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] in
143 theorem operator_integrable (a : A) : Integrable (operator D P a) μ := by
144   have hi (i : I) : Integrable ((P.cell i).indicator (fun _ : Y => cellAverage D P a i)) μ :=
145     (integrable_const (μ := μ) (cellAverage D P a i)).indicator (P.measurable i)
146   exact integrable_finsetSum (f := fun i => (P.cell i).indicator
147     (fun _ : Y => cellAverage D P a i)) Finset.univ (fun i _ => hi i)
148 
149 omit [MeasurableSpace E] [BorelSpace E] [IsProbabilityMeasure μ] in
150 /-- Every cell event operator agrees exactly, despite changing fine densities. -/
151 theorem exact_cell_operator (a : A) (i : I) :
152     cellOperator μ (operator D P a) (P.cell i)=cellOperator μ (D.op a) (P.cell i) := by
153   unfold cellOperator
154   rw [setIntegral_congr_fun (P.measurable i) (fun y hy => operator_on_cell D P a i hy),setIntegral_const]
155   change μ.real (P.cell i) • ((μ.real (P.cell i))⁻¹ • _)=_
156   rw [smul_smul,mul_inv_cancel₀ (P.mass_positive i).ne',one_smul]
157   rfl
158 
159 omit [MeasurableSpace E] [BorelSpace E] in
160 theorem integral_operator (a : A) :
161     (∫ y,operator D P a y∂μ)=∫ y,D.op a y∂μ := by
162   rw [P.integral_partition _ (operator_integrable D P a),P.integral_partition _ (D.integrable_op a)]
163   apply Finset.sum_congr rfl
164   intro i _
165   exact exact_cell_operator D P a i
166 
167 /-- Positivity, measurability, integrability and exact integrated mass are
168 proved for the actual lifted cell average. -/
169 noncomputable def instrument : DensityInstrument (A := A) C μ where
170   op := operator D P
171   measurable_op := operator_measurable D P
172   integrable_op := operator_integrable D P
173   positive a := Filter.Eventually.of_forall (fun y z hz => operator_positive D P a y hz)
174   mass_preserving a z := by rw [integral_operator D P a];exact D.mass_preserving a z
175 
176 omit [MeasurableSpace E] [BorelSpace E] in
177 /-- Subtracting the true cell average is an actual integral of differences. -/
178 theorem difference_eq_average (a : A) (i : I) (y : Y) (z : E) :
179     D.op a y z-cellAverage D P a i z=
180       (μ.real (P.cell i))⁻¹ • ∫ v in P.cell i,D.op a y z-D.op a v z∂μ := by
181   rw [integral_sub (integrable_const _).integrableOn (D.applied_integrable a z).integrableOn,
182     setIntegral_const]
183   rw [smul_sub,smul_smul,inv_mul_cancel₀ (P.mass_positive i).ne',one_smul]
184   rw [cellAverage,smul_apply,
185     cellOperator_apply μ (D.op a) (D.integrable_op a) (P.cell i) z]
186 
187 omit [MeasurableSpace E] [BorelSpace E] in
188 theorem discrepancy_integrable (a : A) (z : E) :
189     Integrable (fun y => C.value ((D.op a y-operator D P a y) z)) μ := by
190   exact C.integrable_value ((D.applied_integrable a z).sub
191     ((ContinuousLinearMap.apply ℝ E z).integrable_comp (operator_integrable D P a)))
192 
193 /-- Actual integrated base-norm discrepancy for an action and input state. -/
194 noncomputable def discrepancy (a : A) (z : E) : ℝ :=
195   ∫ y,C.value ((D.op a y-operator D P a y) z)∂μ
196 
197 /-- The supremum over normalized states/actions, with the harmless zero
198 included to give value zero when that index set is empty. -/
199 noncomputable def approximationError : ℝ :=
200   sSup (insert 0 {r | ∃ a z,z∈C.base ∧ r=discrepancy D P a z})
201 
202 variable [PseudoMetricSpace Y] [BorelSpace Y]
203 
204 /-- The source induced-norm Lipschitz assumption, restricted only to pairs
205 inside the same cells where averaging actually uses it. -/
206 def CellLipschitz (L : ℝ) : Prop := ∀ a i,∀ y∈P.cell i,∀ v∈P.cell i,
207   inducedNorm (C := C) (D.op a y-D.op a v)≤L*dist y v
208 
209 /-- Operational form of every cell having diameter at most h. -/
210 def CellDiameter (h : ℝ) : Prop := ∀ i,∀ y∈P.cell i,∀ v∈P.cell i,dist y v≤h
211 
212 omit [MeasurableSpace E] [BorelSpace E] in
213 theorem distance_integrable_cell {h : ℝ} (hd : CellDiameter P h)
214     (i : I) (y : Y) (hy : y∈P.cell i) :
215     IntegrableOn (fun v => dist y v) (P.cell i) μ := by
216   have hm : AEStronglyMeasurable (fun v : Y => dist y v) (μ.restrict (P.cell i)) :=
217     (continuous_const.dist continuous_id).measurable.aestronglyMeasurable
218   apply (integrable_const h).mono' hm
219   filter_upwards [ae_restrict_mem (P.measurable i)] with v hv
220   rw [Real.norm_eq_abs,abs_of_nonneg dist_nonneg]
221   exact hd i y hy v hv
222 
223 omit [MeasurableSpace E] [BorelSpace E] in
224 /-- The averaging inequality is derived from the genuine integral triangle
225 inequality and the induced operator norm, not imposed as a certificate field. -/
226 theorem point_error_pair_bound {L h : ℝ} (hl : CellLipschitz D P L)
227     (hd : CellDiameter P h) (a : A) (i : I) (y : Y) (hy : y∈P.cell i)
228     (z : E) (hz : z∈C.base) :
229     C.value (D.op a y z-cellAverage D P a i z)≤
230       (μ.real (P.cell i))⁻¹*L*(∫ v in P.cell i,dist y v∂μ) := by
231   have hf : Integrable (fun v => D.op a y z-D.op a v z) (μ.restrict (P.cell i)) :=
232     ((integrable_const _).sub (D.applied_integrable a z)).integrableOn
233   have hv : C.value z=1 := (C.value_on_cone hz.1).trans hz.2
234   have hb : (∫ v in P.cell i,C.value (D.op a y z-D.op a v z)∂μ)≤
235       ∫ v in P.cell i,L*dist y v∂μ := by
236     apply integral_mono_ae (C.integrable_value hf) ((distance_integrable_cell P hd i y hy).const_mul L)
237     filter_upwards [ae_restrict_mem (P.measurable i)] with v hv'
238     have ha := value_apply_le_inducedNorm (C := C) (D.op a y-D.op a v) z
239     rw [hv,mul_one] at ha
240     exact ha.trans (hl a i y hy v hv')
241   rw [difference_eq_average D P a i y z,C.value_smul_of_nonneg
242     (inv_nonneg.mpr (P.mass_positive i).le)]
243   calc
244     _ ≤ (μ.real (P.cell i))⁻¹*(∫ v in P.cell i,C.value (D.op a y z-D.op a v z)∂μ) :=
245       mul_le_mul_of_nonneg_left (C.value_integral_le_integral_value hf)
246         (inv_nonneg.mpr (P.mass_positive i).le)
247     _ ≤ (μ.real (P.cell i))⁻¹*(∫ v in P.cell i,L*dist y v∂μ) :=
248       mul_le_mul_of_nonneg_left hb (inv_nonneg.mpr (P.mass_positive i).le)
249     _ = _ := by rw [integral_const_mul];ring
250 
251 end Komorebi.LSM.PositiveCellApproximation

Back to source controls