PositiveCellResolution.lean

1 import KomorebiLSM.PositiveCellApproximation
2 
3 /-! P58 resolution bounds for the literal positive cell-average density. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.PositiveCellApproximation
6 open MeasureTheory ContinuousInstrument ContinuousBins
7 open scoped BigOperators
8 variable {E A I : Type*} [Fintype I]
9 variable [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
10 variable [MeasurableSpace E] [BorelSpace E]
11 variable {C : BaseNorm.ProbabilityCone E}
12 
13 section Metric
14 variable {Y : Type*} [MeasurableSpace Y] [PseudoMetricSpace Y] [BorelSpace Y]
15 variable {μ : Measure Y} [IsProbabilityMeasure μ]
16 variable (D : DensityInstrument (A := A) C μ) (P : CellPartition μ I)
17 
18 omit [MeasurableSpace E] [BorelSpace E] in
19 theorem point_error_diameter {L h : ℝ} (hL : 0≤L) (hl : CellLipschitz D P L)
20     (hd : CellDiameter P h) (a : A) (i : I) (y : Y) (hy : y∈P.cell i)
21     (z : E) (hz : z∈C.base) :
22     C.value (D.op a y z-cellAverage D P a i z)≤L*h := by
23   have hb : (∫ v in P.cell i,dist y v∂μ)≤μ.real (P.cell i)*h := by
24     calc
25       _ ≤ ∫ _ in P.cell i,h∂μ := by
26         apply integral_mono_ae (distance_integrable_cell P hd i y hy) (integrable_const h)
27         filter_upwards [ae_restrict_mem (P.measurable i)] with v hv
28         exact hd i y hy v hv
29       _ = _ := by rw [setIntegral_const,smul_eq_mul]
30   calc
31     _ ≤ (μ.real (P.cell i))⁻¹*L*(∫ v in P.cell i,dist y v∂μ) :=
32       point_error_pair_bound D P hl hd a i y hy z hz
33     _ ≤ (μ.real (P.cell i))⁻¹*L*(μ.real (P.cell i)*h) :=
34       mul_le_mul_of_nonneg_left hb (mul_nonneg (inv_nonneg.mpr (P.mass_positive i).le) hL)
35     _ = _ := by field_simp [(P.mass_positive i).ne']
36 
37 omit [MeasurableSpace E] [BorelSpace E] in
38 /-- Integrating the pointwise diameter estimate uses the actual probability
39 reference and actual base-norm discrepancy. -/
40 theorem discrepancy_le_diameter {L h : ℝ} (hL : 0≤L) (hl : CellLipschitz D P L)
41     (hd : CellDiameter P h) (a : A) (z : E) (hz : z∈C.base) :
42     discrepancy D P a z≤L*h := by
43   unfold discrepancy
44   calc
45     _ ≤ ∫ _ : Y,L*h∂μ := by
46       apply integral_mono_ae (discrepancy_integrable D P a z) (integrable_const _)
47       filter_upwards [P.cover] with y hy
48       obtain ⟨i,hi⟩ := hy
49       rw [operator_on_cell D P a i hi]
50       exact point_error_diameter D P hL hl hd a i y hi z hz
51     _ = _ := by simp
52 
53 omit [PseudoMetricSpace Y] [BorelSpace Y] [MeasurableSpace E] [BorelSpace E]
54   [FiniteDimensional ℝ E] [IsProbabilityMeasure μ] in
55 theorem approximationError_le {r : ℝ} (hr : 0≤r)
56     (hb : ∀ a z,z∈C.base → discrepancy D P a z≤r) : approximationError D P≤r := by
57   apply csSup_le ⟨0,Set.mem_insert _ _⟩
58   rintro q (rfl | ⟨a,z,hz,rfl⟩)
59   · exact hr
60   · exact hb a z hz
61 
62 omit [PseudoMetricSpace Y] [BorelSpace Y] [MeasurableSpace E] [BorelSpace E]
63   [FiniteDimensional ℝ E] [IsProbabilityMeasure μ] in
64 /-- Whenever normalized action/state inputs exist, inserting zero does not
65 change the ordinary source supremum, since every actual discrepancy is nonnegative. -/
66 theorem approximationError_eq_sup (hn : ∃ _a : A,∃ z : E,z∈C.base)
67     (hb : BddAbove {r | ∃ a z,z∈C.base ∧ r=discrepancy D P a z}) :
68     approximationError D P=sSup {r | ∃ a z,z∈C.base ∧ r=discrepancy D P a z} := by
69   let S : Set ℝ := {r | ∃ a z,z∈C.base ∧ r=discrepancy D P a z}
70   change sSup (insert 0 S)=sSup S
71   obtain ⟨a,z,hz⟩ := hn
72   have hm : discrepancy D P a z∈S := ⟨a,z,hz,rfl⟩
73   have hs : S.Nonempty := ⟨_,hm⟩
74   have hnonneg : 0≤sSup S :=
75     (integral_nonneg (fun y => C.value_nonneg ((D.op a y-operator D P a y) z))).trans
76       (le_csSup hb hm)
77   have hb' : BddAbove (insert 0 S) := by
78     obtain ⟨r,hr⟩ := hb
79     refine ⟨max 0 r,?_⟩
80     rintro q (rfl | hq)
81     · exact le_max_left _ _
82     · exact (hr hq).trans (le_max_right _ _)
83   apply le_antisymm
84   · apply csSup_le ⟨0,Set.mem_insert _ _⟩
85     rintro q (rfl | hq)
86     · exact hnonneg
87     · exact le_csSup hb hq
88   · apply csSup_le hs
89     intro q hq
90     exact le_csSup hb' (Set.mem_insert_of_mem 0 hq)
91 
92 omit [MeasurableSpace E] [BorelSpace E] in
93 /-- The full supremum in P58 is bounded by L times the cell diameter. -/
94 theorem approximationError_le_diameter {L h : ℝ} (hL : 0≤L) (hh : 0≤h)
95     (hl : CellLipschitz D P L) (hd : CellDiameter P h) :
96     approximationError D P≤L*h :=
97   approximationError_le D P (mul_nonneg hL hh)
98     (fun a z hz => discrepancy_le_diameter D P hL hl hd a z hz)
99 
100 end Metric
101 end Komorebi.LSM.PositiveCellApproximation

Back to source controls