PositiveCellUniform.lean

1 import KomorebiLSM.PositiveCellResolution
2 
3 /-! The sharper P58 bound uses actual double-distance integrals in the fixed
4 uniform reference on [-1,1], not a postulated numerical averaging constant. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.PositiveCellApproximation
7 open MeasureTheory ContinuousInstrument ContinuousBins
8 open scoped BigOperators
9 variable {I : Type*} [Fintype I]
10 variable (P : CellPartition UniformIntervalMoments.measure I)
11 
12 noncomputable def cellDistance (i : I) (y : ℝ) : ℝ :=
13   ∫ v in P.cell i,dist y v∂UniformIntervalMoments.measure
14 
15 noncomputable def resolution : ℝ :=
16   ∑ i,(UniformIntervalMoments.measure.real (P.cell i))⁻¹*
17     ∫ y in P.cell i,cellDistance P i y∂UniformIntervalMoments.measure
18 
19 theorem cellDistance_nonneg (i : I) (y : ℝ) : 0≤cellDistance P i y :=
20   integral_nonneg (fun _ => dist_nonneg)
21 
22 theorem cellDistance_stronglyMeasurable (i : I) : StronglyMeasurable (cellDistance P i) := by
23   have hm : StronglyMeasurable (fun p : ℝ × ℝ => dist p.1 p.2) :=
24     (continuous_fst.dist continuous_snd).stronglyMeasurable
25   exact hm.integral_prod_right
26 
27 theorem cellDistance_le {h : ℝ} (hd : CellDiameter P h)
28     (i : I) (y : ℝ) (hy : y∈P.cell i) :
29     cellDistance P i y≤UniformIntervalMoments.measure.real (P.cell i)*h := by
30   calc
31     _ ≤ ∫ _ in P.cell i,h∂UniformIntervalMoments.measure := by
32       apply integral_mono_ae (distance_integrable_cell P hd i y hy) (integrable_const h)
33       filter_upwards [ae_restrict_mem (P.measurable i)] with v hv
34       exact hd i y hy v hv
35     _ = _ := by rw [setIntegral_const,smul_eq_mul]
36 
37 theorem cellDistance_integrable {h : ℝ} (hd : CellDiameter P h) (i : I) :
38     IntegrableOn (cellDistance P i) (P.cell i) UniformIntervalMoments.measure := by
39   apply (integrable_const (UniformIntervalMoments.measure.real (P.cell i)*h)).mono'
40     (cellDistance_stronglyMeasurable P i).aestronglyMeasurable
41   filter_upwards [ae_restrict_mem (P.measurable i)] with y hy
42   rw [Real.norm_eq_abs,abs_of_nonneg (cellDistance_nonneg P i y)]
43   exact cellDistance_le P hd i y hy
44 
45 /-- The factor h/3 is calculated from the actual uniform cell measure. -/
46 theorem resolution_equal_intervals (a b : I → ℝ) (h : ℝ) (hh : 0<h)
47     (hc : ∀ i,P.cell i=Set.Ioc (a i) (b i))
48     (ha : ∀ i,-1≤a i) (hb : ∀ i,b i≤1) (hw : ∀ i,b i-a i=h) :
49     resolution P=h/3 := by
50   have hab (i : I) : a i<b i := by linarith [hw i]
51   have hm (i : I) : UniformIntervalMoments.measure.real (P.cell i)=h/2 := by
52     rw [hc i,CellDistance.uniform_cell_mass (a i) (b i) (ha i) (hb i) (hab i).le,hw i]
53   have hd (i : I) : (∫ y in P.cell i,cellDistance P i y∂UniformIntervalMoments.measure)=h^3/12 := by
54     unfold cellDistance
55     simp only [hc i]
56     rw [CellDistance.uniform_cell_double_distance (a i) (b i) (ha i) (hb i) (hab i).le,hw i]
57   calc
58     resolution P=∑ i,UniformIntervalMoments.measure.real (P.cell i)*h/3 := by
59       unfold resolution
60       apply Finset.sum_congr rfl
61       intro i _
62       rw [hm i,hd i]
63       field_simp [hh.ne']; ring
64     _ = (∑ i,UniformIntervalMoments.measure.real (P.cell i))*h/3 := by
65       simp only [div_eq_mul_inv,Finset.sum_mul]
66     _ = h/3 := by rw [P.total_mass,one_mul]
67 
68 theorem diameter_equal_intervals (a b : I → ℝ) (h : ℝ)
69     (hc : ∀ i,P.cell i=Set.Ioc (a i) (b i)) (hw : ∀ i,b i-a i=h) :
70     CellDiameter P h := by
71   intro i y hy v hv
72   rw [hc i] at hy hv
73   rw [Real.dist_eq]
74   apply abs_le.mpr
75   constructor <;> linarith [hw i,hy.1,hy.2,hv.1,hv.2]
76 
77 variable {E A : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
78 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
79 variable {C : BaseNorm.ProbabilityCone E}
80 variable (D : DensityInstrument (A := A) C UniformIntervalMoments.measure)
81 
82 omit [MeasurableSpace E] [BorelSpace E] in
83 theorem cell_error_pair_integral {L h : ℝ} (hl : CellLipschitz D P L) (hd : CellDiameter P h)
84     (a : A) (i : I) (z : E) (hz : z∈C.base) :
85     (∫ y in P.cell i,C.value ((D.op a y-operator D P a y) z)∂UniformIntervalMoments.measure)≤
86       (UniformIntervalMoments.measure.real (P.cell i))⁻¹*L*
87         (∫ y in P.cell i,cellDistance P i y∂UniformIntervalMoments.measure) := by
88   have hb : (∫ y in P.cell i,C.value ((D.op a y-operator D P a y) z)∂UniformIntervalMoments.measure)≤
89       ∫ y in P.cell i,(UniformIntervalMoments.measure.real (P.cell i))⁻¹*L*cellDistance P i y
90         ∂UniformIntervalMoments.measure := by
91     apply integral_mono_ae (discrepancy_integrable D P a z).integrableOn
92       ((cellDistance_integrable P hd i).const_mul _)
93     filter_upwards [ae_restrict_mem (P.measurable i)] with y hy
94     rw [operator_on_cell D P a i hy]
95     exact point_error_pair_bound D P hl hd a i y hy z hz
96   exact hb.trans_eq (integral_const_mul _ _)
97 
98 omit [MeasurableSpace E] [BorelSpace E] in
99 theorem discrepancy_le_resolution {L h : ℝ} (hl : CellLipschitz D P L) (hd : CellDiameter P h)
100     (a : A) (z : E) (hz : z∈C.base) : discrepancy D P a z≤L*resolution P := by
101   unfold discrepancy
102   rw [P.integral_partition _ (discrepancy_integrable D P a z)]
103   calc
104     _ ≤ ∑ i,(UniformIntervalMoments.measure.real (P.cell i))⁻¹*L*
105         (∫ y in P.cell i,cellDistance P i y∂UniformIntervalMoments.measure) :=
106       Finset.sum_le_sum (fun i _ => cell_error_pair_integral P D hl hd a i z hz)
107     _ = _ := by
108       unfold resolution
109       rw [Finset.mul_sum]
110       apply Finset.sum_congr rfl
111       intro i _
112       ring
113 
114 omit [MeasurableSpace E] [BorelSpace E] in
115 /-- Equal intervals in the actual uniform[-1,1] reference have error Lh/3.
116 The hypotheses are a genuine interval partition and an induced-norm bound on
117 the interval; the averaging bound and the factor one third are proved. -/
118 theorem approximationError_le_equal_intervals (a b : I → ℝ) (h L : ℝ)
119     (hh : 0<h) (hL : 0≤L) (hc : ∀ i,P.cell i=Set.Ioc (a i) (b i))
120     (ha : ∀ i,-1≤a i) (hb : ∀ i,b i≤1) (hw : ∀ i,b i-a i=h)
121     (hl : ∀ a,∀ y∈Set.Icc (-1 : ℝ) 1,∀ v∈Set.Icc (-1 : ℝ) 1,
122       inducedNorm (C := C) (D.op a y-D.op a v)≤L*dist y v) :
123     approximationError D P≤L*h/3 := by
124   have hd := diameter_equal_intervals P a b h hc hw
125   have hcell : CellLipschitz D P L := by
126     intro act i y hy v hv
127     rw [hc i] at hy hv
128     exact hl act y ⟨le_trans (ha i) hy.1.le,le_trans hy.2 (hb i)⟩
129       v ⟨le_trans (ha i) hv.1.le,le_trans hv.2 (hb i)⟩
130   apply approximationError_le D P (div_nonneg (mul_nonneg hL hh.le) (by norm_num))
131   intro act z hz
132   have he := discrepancy_le_resolution P D hcell hd act z hz
133   rw [resolution_equal_intervals P a b h hh hc ha hb hw] at he
134   nlinarith
135 
136 end Komorebi.LSM.PositiveCellApproximation

Back to source controls