RobustOrientedMargin.lean

1 import KomorebiLSM.LorentzCylinder
2 import KomorebiLSM.PolynomialGram
3 import KomorebiLSM.ContinuousRecords
4 
5 /-! P71: an actual minimum margin on the normalized Lorentz base controls
6 orientation and spatial uncertainty before normalization. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.RobustOrientedMargin
9 open LorentzCylinder MeasureTheory
10 open scoped BigOperators
11 variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
12 
13 /-- Oriented, unnormalized distance from the Lorentz boundary. -/
14 def slack (z : State V) : ℝ := z.1-‖z.2‖
15 
16 omit [NormedSpace ℝ V] in
17 theorem slack_add_lower (w d : State V) :
18     slack w-|d.1|-‖d.2‖≤slack (w+d) := by
19   change w.1-‖w.2‖-|d.1|-‖d.2‖≤w.1+d.1-‖w.2+d.2‖
20   linarith [norm_add_le w.2 d.2,neg_abs_le d.1]
21 
22 variable [FiniteDimensional ℝ V]
23 
24 /-- The minimum is attained on the actual entire normalized spatial ball. -/
25 theorem exists_minimum (F : State V →L[ℝ] State V) :
26     ∃ v : V,‖v‖≤1 ∧ ∀ w : V,‖w‖≤1 → slack (F (1,v))≤slack (F (1,w)) := by
27   have hc : IsCompact {v : V | ‖v‖≤1} := by
28     simpa only [Metric.closedBall,dist_zero_right] using isCompact_closedBall (0 : V) 1
29   have hn : ({v : V | ‖v‖≤1}).Nonempty := ⟨0,by simp⟩
30   have hf : Continuous (fun v : V => slack (F (1,v))) := by
31     exact ((F.continuous.comp (continuous_const.prodMk continuous_id)).fst).sub
32       ((F.continuous.comp (continuous_const.prodMk continuous_id)).snd.norm)
33   obtain ⟨v,hv,hmin⟩ := hc.exists_isMinOn hn hf.continuousOn
34   exact ⟨v,hv,hmin⟩
35 
36 noncomputable def worstInput (F : State V →L[ℝ] State V) : V := (exists_minimum F).choose
37 noncomputable def sigma (F : State V →L[ℝ] State V) : ℝ := slack (F (1,worstInput F))
38 
39 theorem worstInput_mem (F : State V →L[ℝ] State V) : ‖worstInput F‖≤1 :=
40   (exists_minimum F).choose_spec.1
41 
42 theorem sigma_le (F : State V →L[ℝ] State V) (v : V) (hv : ‖v‖≤1) :
43     sigma F≤slack (F (1,v)) := (exists_minimum F).choose_spec.2 v hv
44 
45 /-- Thus a sigma bound is exactly a bound on every normalized input, not a grid. -/
46 theorem le_sigma_iff (F : State V →L[ℝ] State V) (kappa : ℝ) :
47     kappa≤sigma F ↔ ∀ v : V,‖v‖≤1 → kappa≤slack (F (1,v)) := by
48   constructor
49   · intro h v hv
50     exact h.trans (sigma_le F v hv)
51   · intro h
52     exact h (worstInput F) (worstInput_mem F)
53 
54 /-- The residual slack is derived from the actual minimum and literal output errors. -/
55 theorem normalized_residual (F Delta : State V →L[ℝ] State V) (kappa e0 e1 : ℝ)
56     (hmargin : kappa≤sigma F)
57     (h0 : ∀ v : V,‖v‖≤1 → |(Delta (1,v)).1|≤e0)
58     (h1 : ∀ v : V,‖v‖≤1 → ‖(Delta (1,v)).2‖≤e1)
59     (v : V) (hv : ‖v‖≤1) : kappa-e0-e1≤slack ((F+Delta) (1,v)) := by
60   have hm := hmargin.trans (sigma_le F v hv)
61   have he0 := h0 v hv
62   have he1 := h1 v hv
63   have ha := slack_add_lower (F (1,v)) (Delta (1,v))
64   change kappa-e0-e1≤slack (F (1,v)+Delta (1,v))
65   linarith
66 
67 /-- The actual minimum margin of the uncertain branch retains the residual slack. -/
68 theorem residual_margin (F Delta : State V →L[ℝ] State V) (kappa e0 e1 : ℝ)
69     (hmargin : kappa≤sigma F)
70     (h0 : ∀ v : V,‖v‖≤1 → |(Delta (1,v)).1|≤e0)
71     (h1 : ∀ v : V,‖v‖≤1 → ‖(Delta (1,v)).2‖≤e1) :
72     kappa-e0-e1≤sigma (F+Delta) :=
73   (le_sigma_iff (F+Delta) _).mpr (fun v hv => normalized_residual F Delta kappa e0 e1 hmargin h0 h1 v hv)
74 
75 omit [FiniteDimensional ℝ V] in
76 /-- Homogeneity extends normalized preservation to the entire cone, including zero mass. -/
77 theorem preserves_of_normalized (G : State V →L[ℝ] State V)
78     (hG : ∀ v : V,‖v‖≤1 → G (1,v)∈cone) {z : State V} (hz : z∈cone) : G z∈cone := by
79   have hm : 0≤z.1 := (norm_nonneg _).trans hz
80   by_cases hm0 : z.1=0
81   · have hz0 : z=0 := (probabilityCone.mass_zero_iff hz).mp hm0
82     rw [hz0,map_zero]
83     exact probabilityCone.zero_mem
84   · have hmp : 0<z.1 := lt_of_le_of_ne hm (Ne.symm hm0)
85     have hv : ‖z.1⁻¹ • z.2‖≤1 := by
86       rw [norm_smul,Real.norm_eq_abs,abs_of_pos (inv_pos.mpr hmp)]
87       exact (inv_mul_le_iff₀ hmp).mpr (by simpa using hz)
88     have he : z=z.1 • (1,z.1⁻¹ • z.2) := by
89       apply Prod.ext
90       · simp
91       · change z.2=z.1 • (z.1⁻¹ • z.2)
92         rw [smul_smul,mul_inv_cancel₀ hm0,one_smul]
93     rw [he,map_smul]
94     exact probabilityCone.smul_mem hm (hG _ hv)
95 
96 /-- P71 cone preservation follows from the oriented margin and the two error bounds. -/
97 theorem robust_preserves (F Delta : State V →L[ℝ] State V) (kappa e0 e1 : ℝ)
98     (hmargin : kappa≤sigma F)
99     (h0 : ∀ v : V,‖v‖≤1 → |(Delta (1,v)).1|≤e0)
100     (h1 : ∀ v : V,‖v‖≤1 → ‖(Delta (1,v)).2‖≤e1)
101     (hcover : e0+e1≤kappa) {z : State V} (hz : z∈cone) : (F+Delta) z∈cone := by
102   apply preserves_of_normalized (F+Delta) _ hz
103   intro v hv
104   have hr := normalized_residual F Delta kappa e0 e1 hmargin h0 h1 v hv
105   change ‖((F+Delta) (1,v)).2‖≤((F+Delta) (1,v)).1
106   unfold slack at hr
107   linarith
108 
109 theorem strict_residual (F Delta : State V →L[ℝ] State V) (kappa e0 e1 : ℝ)
110     (hmargin : kappa≤sigma F)
111     (h0 : ∀ v : V,‖v‖≤1 → |(Delta (1,v)).1|≤e0)
112     (h1 : ∀ v : V,‖v‖≤1 → ‖(Delta (1,v)).2‖≤e1)
113     (hstrict : e0+e1<kappa) (v : V) (hv : ‖v‖≤1) :
114     0<kappa-e0-e1 ∧ kappa-e0-e1≤slack ((F+Delta) (1,v)) :=
115   ⟨by linarith,normalized_residual F Delta kappa e0 e1 hmargin h0 h1 v hv⟩
116 
117 omit [FiniteDimensional ℝ V] in
118 /-- Positive-density branches have a normalized cone state; the premise is not floored. -/
119 theorem positive_posterior {G : State V →L[ℝ] State V}
120     (hG : ∀ z∈cone,G z∈cone) {z : State V} (hz : z∈cone) (hp : 0<(G z).1) :
121     ((G z).1⁻¹ • G z)∈probabilityCone.base := by
122   refine ⟨probabilityCone.smul_mem (inv_nonneg.mpr hp.le) (hG z hz),?_⟩
123   change (G z).1⁻¹*(G z).1=1
124   exact inv_mul_cancel₀ hp.ne'
125 
126 section Polynomial
127 variable {A : Type*} {n : ℕ}
128 
129 omit [FiniteDimensional ℝ V] in
130 theorem polynomial_add (F Delta : Fin n → State V →L[ℝ] State V) (u : ℝ) :
131     PolynomialGram.operatorPolynomial (fun k => F k+Delta k) u=
132       PolynomialGram.operatorPolynomial F u+PolynomialGram.operatorPolynomial Delta u := by
133   simp only [PolynomialGram.operatorPolynomial,smul_add,Finset.sum_add_distrib]
134 
135 /-- Complete interval margin data, with no desired cone-invariance conclusion supplied. -/
136 structure MarginCertificate (F Delta : A → Fin n → State V →L[ℝ] State V)
137     (kappa e0 e1 : A → ℝ → ℝ) where
138   margin : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → kappa a u≤sigma (PolynomialGram.operatorPolynomial (F a) u)
139   mass_error : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : V,‖v‖≤1 →
140     |(PolynomialGram.operatorPolynomial (Delta a) u (1,v)).1|≤e0 a u
141   spatial_error : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : V,‖v‖≤1 →
142     ‖(PolynomialGram.operatorPolynomial (Delta a) u (1,v)).2‖≤e1 a u
143   cover : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → e0 a u+e1 a u≤kappa a u
144 
145 /-- Every certified interval value preserves the cone pointwise, including endpoints. -/
146 theorem MarginCertificate.preserves {F Delta : A → Fin n → State V →L[ℝ] State V}
147     {kappa e0 e1 : A → ℝ → ℝ} (cert : MarginCertificate F Delta kappa e0 e1)
148     (a : A) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1) {z : State V} (hz : z∈cone) :
149     PolynomialGram.operatorPolynomial (fun k => F a k+Delta a k) u z∈cone := by
150   rw [polynomial_add]
151   exact robust_preserves _ _ _ _ _ (cert.margin a u hu) (cert.mass_error a u hu)
152     (cert.spatial_error a u hu) (cert.cover a u hu) hz
153 
154 variable [MeasurableSpace V] [BorelSpace V]
155 
156 /-- The uncertain polynomial itself is the literal valid observation density. -/
157 noncomputable def uncertainInstrument (F Delta : A → Fin n → State V →L[ℝ] State V)
158     (kappa e0 e1 : A → ℝ → ℝ) (cert : MarginCertificate F Delta kappa e0 e1)
159     (hm : ∀ a z,probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • (F a k+Delta a k)) z)=
160       probabilityCone.mass z) :
161     ContinuousInstrument.DensityInstrument (A := A) (probabilityCone (V := V)) UniformIntervalMoments.measure where
162   op a := PolynomialGram.operatorPolynomial (fun k => F a k+Delta a k)
163   measurable_op a := (PolynomialGram.operatorPolynomial_continuous _).measurable
164   integrable_op a := PolynomialGram.operatorPolynomial_integrable _
165   positive a := by
166     filter_upwards [PolynomialGram.uniform_ae_interval] with u hu
167     intro z hz
168     rw [polynomial_add]
169     exact robust_preserves _ _ _ _ _ (cert.margin a u hu) (cert.mass_error a u hu)
170       (cert.spatial_error a u hu) (cert.cover a u hu) hz
171   mass_preserving a z := by
172     rw [PolynomialGram.operatorPolynomial_integral]
173     exact hm a z
174 
175 theorem uncertain_record_probability [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
176     (F Delta : A → Fin n → State V →L[ℝ] State V) (kappa e0 e1 : A → ℝ → ℝ)
177     (cert : MarginCertificate F Delta kappa e0 e1)
178     (hm : ∀ a z,probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • (F a k+Delta a k)) z)=
179       probabilityCone.mass z)
180     (policy : ContinuousRecords.Policy (A := A) (Y := ℝ)) (z : State V)
181     (hz : z∈probabilityCone.base) (horizon : ℕ) :
182     IsProbabilityMeasure (ContinuousRecords.recordLaw (uncertainInstrument F Delta kappa e0 e1 cert hm)
183       policy z horizon) :=
184   ContinuousRecords.recordLaw_probability (uncertainInstrument F Delta kappa e0 e1 cert hm)
185     policy ⟨z,hz⟩ horizon
186 
187 end Polynomial
188 
189 section Atlas
190 variable {E A : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
191   [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
192   [MeasurableSpace V] [BorelSpace V] {n : ℕ}
193 
194 /-- Inverse conjugation uses the actual atlas, with its actual inverse. -/
195 noncomputable def pullbackOperator (T : E ≃ₗ[ℝ] State V) (G : State V →L[ℝ] State V) : E →L[ℝ] E :=
196   (T.symm.toLinearMap.comp (G.toLinearMap.comp T.toLinearMap)).toContinuousLinearMap
197 
198 omit [FiniteDimensional ℝ V] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace V] [BorelSpace V] in
199 @[simp] theorem pullbackOperator_action (T : E ≃ₗ[ℝ] State V)
200     (G : State V →L[ℝ] State V) (z : E) : T (pullbackOperator T G z)=G (T z) := by
201   change T (T.symm (G (T z)))=_
202   exact T.apply_symm_apply _
203 
204 omit [FiniteDimensional ℝ V] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace V] [BorelSpace V] in
205 theorem pullback_weighted_action (T : E ≃ₗ[ℝ] State V)
206     (G : Fin n → State V →L[ℝ] State V) (weights : Fin n → ℝ) (z : E) :
207     T ((∑ k : Fin n,weights k • pullbackOperator T (G k)) z)=
208       (∑ k : Fin n,weights k • G k) (T z) := by
209   simp only [sum_apply,smul_apply,map_sum,map_smul,pullbackOperator_action]
210 
211 omit [FiniteDimensional ℝ V] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace V] [BorelSpace V] in
212 /-- Original and transported polynomial densities are the same linear family in different coordinates. -/
213 theorem pullback_polynomial_action (T : E ≃ₗ[ℝ] State V)
214     (G : Fin n → State V →L[ℝ] State V) (u : ℝ) (z : E) :
215     T (PolynomialGram.operatorPolynomial (fun k => pullbackOperator T (G k)) u z)=
216       PolynomialGram.operatorPolynomial G u (T z) :=
217   pullback_weighted_action T G (fun k => u^(k:ℕ)) z
218 
219 omit [FiniteDimensional ℝ V] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace V] [BorelSpace V] in
220 /-- The explicit mass-preservation premise identifies the original declared mass row. -/
221 theorem atlas_mass_agrees (T : E ≃ₗ[ℝ] State V) (l : E →ₗ[ℝ] ℝ)
222     (hT : ∀ z,l z=(T z).1) : (atlasCone T).mass=l := by
223   apply LinearMap.ext
224   intro z
225   exact (hT z).symm
226 
227 omit [FiniteDimensional ℝ V] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace V] [BorelSpace V] in
228 /-- This is exactly the normalized domain K_T from the source. -/
229 theorem atlas_base_iff (T : E ≃ₗ[ℝ] State V) (z : E) :
230     z∈(atlasCone T).base ↔ ∃ v : V,‖v‖≤1 ∧ z=T.symm (1,v) := by
231   constructor
232   · rintro ⟨hz,hm⟩
233     change ‖(T z).2‖≤(T z).1 at hz
234     change (T z).1=1 at hm
235     refine ⟨(T z).2,hz.trans_eq hm,?_⟩
236     apply T.injective
237     rw [T.apply_symm_apply]
238     exact Prod.ext hm rfl
239   · rintro ⟨v,hv,rfl⟩
240     change (T (T.symm (1,v))∈cone ∧ (T (T.symm (1,v))).1=1)
241     rw [T.apply_symm_apply]
242     exact ⟨hv,rfl⟩
243 
244 omit [FiniteDimensional ℝ V] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace V] [BorelSpace V] in
245 /-- Exact integrated mass can equivalently be checked in the original coordinates. -/
246 theorem atlas_moment_mass_iff (T : E ≃ₗ[ℝ] State V)
247     (G : Fin n → State V →L[ℝ] State V) :
248     (∀ z,(atlasCone T).mass ((∑ k : Fin n,UniformIntervalMoments.moment k • pullbackOperator T (G k)) z)=
249       (atlasCone T).mass z) ↔
250     (∀ y,probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • G k) y)=probabilityCone.mass y) := by
251   constructor
252   · intro h y
253     have hz := h (T.symm y)
254     change probabilityCone.mass (T ((∑ k : Fin n,UniformIntervalMoments.moment k • pullbackOperator T (G k))
255       (T.symm y)))=probabilityCone.mass (T (T.symm y)) at hz
256     rwa [pullback_weighted_action,T.apply_symm_apply] at hz
257   · intro h z
258     change probabilityCone.mass (T ((∑ k : Fin n,UniformIntervalMoments.moment k • pullbackOperator T (G k)) z))=
259       probabilityCone.mass (T z)
260     rw [pullback_weighted_action]
261     exact h (T z)
262 
263 /-- The literal inverse-conjugated uncertain family is a valid density instrument on K_T. -/
264 noncomputable def atlasUncertainInstrument (T : E ≃ₗ[ℝ] State V)
265     (F Delta : A → Fin n → State V →L[ℝ] State V) (kappa e0 e1 : A → ℝ → ℝ)
266     (cert : MarginCertificate F Delta kappa e0 e1)
267     (hm : ∀ a y,probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • (F a k+Delta a k)) y)=
268       probabilityCone.mass y) :
269     ContinuousInstrument.DensityInstrument (A := A) (atlasCone T) UniformIntervalMoments.measure where
270   op a := PolynomialGram.operatorPolynomial (fun k => pullbackOperator T (F a k+Delta a k))
271   measurable_op a := (PolynomialGram.operatorPolynomial_continuous _).measurable
272   integrable_op a := PolynomialGram.operatorPolynomial_integrable _
273   positive a := by
274     filter_upwards [PolynomialGram.uniform_ae_interval] with u hu
275     intro z hz
276     change T (PolynomialGram.operatorPolynomial (fun k => pullbackOperator T (F a k+Delta a k)) u z)∈cone
277     rw [pullback_polynomial_action,polynomial_add]
278     exact robust_preserves _ _ _ _ _ (cert.margin a u hu) (cert.mass_error a u hu)
279       (cert.spatial_error a u hu) (cert.cover a u hu) hz
280   mass_preserving a z := by
281     rw [PolynomialGram.operatorPolynomial_integral]
282     exact (atlas_moment_mass_iff T (fun k => F a k+Delta a k)).mpr (hm a) z
283 
284 omit [MeasurableSpace V] [BorelSpace V] in
285 /-- A supplied initial state in K_T gives genuine finite laws in the original atlas. -/
286 theorem atlas_record_probability [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
287     (T : E ≃ₗ[ℝ] State V) (F Delta : A → Fin n → State V →L[ℝ] State V)
288     (kappa e0 e1 : A → ℝ → ℝ) (cert : MarginCertificate F Delta kappa e0 e1)
289     (hm : ∀ a y,probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • (F a k+Delta a k)) y)=
290       probabilityCone.mass y)
291     (policy : ContinuousRecords.Policy (A := A) (Y := ℝ)) (z : E)
292     (hz : ∃ v : V,‖v‖≤1 ∧ z=T.symm (1,v)) (horizon : ℕ) :
293     IsProbabilityMeasure (ContinuousRecords.recordLaw (atlasUncertainInstrument T F Delta kappa e0 e1 cert hm)
294       policy z horizon) :=
295   ContinuousRecords.recordLaw_probability (atlasUncertainInstrument T F Delta kappa e0 e1 cert hm)
296     policy ⟨z,(atlas_base_iff T z).mpr hz⟩ horizon
297 end Atlas
298 
299 end Komorebi.LSM.RobustOrientedMargin

Back to source controls