InteriorRepair.lean

1 import KomorebiLSM.RobustOrientedMargin
2 import KomorebiLSM.ContinuousTV
3 
4 /-! P73: a literal center-reset repair buys oriented margin and retains its
5 separate integrated prediction cost in the actual Lorentz base norm. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.InteriorRepair
8 open LorentzCylinder RobustOrientedMargin MeasureTheory ContinuousInstrument
9 open scoped BigOperators
10 variable {V A : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
11 
12 noncomputable def centerReset : State V →L[ℝ] State V :=
13   (ContinuousLinearMap.fst ℝ ℝ V).smulRight (1,0)
14 
15 @[simp] theorem centerReset_apply (z : State V) : centerReset z=(z.1,0) := by
16   change z.1 • (1,(0 : V))=(z.1,0)
17   simp
18 
19 noncomputable def resetOperator (g : ℝ) : State V →L[ℝ] State V := g • centerReset
20 
21 @[simp] theorem resetOperator_normalized (g : ℝ) (v : V) : resetOperator g (1,v)=(g,0) := by
22   simp [resetOperator]
23 
24 @[simp] theorem centerReset_mass (z : State V) : probabilityCone.mass (centerReset z)=probabilityCone.mass z := by
25   rw [centerReset_apply]
26   rfl
27 
28 theorem resetOperator_positive (g : ℝ) (hg : 0≤g) {z : State V} (hz : z∈cone) :
29     resetOperator g z∈cone := by
30   simp only [resetOperator,smul_apply,centerReset_apply]
31   change ‖g • (0 : V)‖≤g*z.1
32   rw [smul_zero,norm_zero]
33   exact mul_nonneg hg ((norm_nonneg _).trans hz)
34 
35 /-- The estimate is not presumed positive. The change is a genuine model mixture. -/
36 noncomputable def repair (Fhat : State V →L[ℝ] State V) (g eta : ℝ) : State V →L[ℝ] State V :=
37   (1-eta) • Fhat+eta • resetOperator g
38 
39 /-- The reset modifies only output mass on normalized inputs. -/
40 theorem repair_slack (Fhat : State V →L[ℝ] State V) (g eta : ℝ)
41     (heta1 : eta≤1) (v : V) :
42     slack (repair Fhat g eta (1,v))=(1-eta)*slack (Fhat (1,v))+eta*g := by
43   simp only [repair,add_apply,smul_apply,resetOperator_normalized]
44   change ((1-eta)*(Fhat (1,v)).1+eta*g)-‖(1-eta) • (Fhat (1,v)).2+eta • (0 : V)‖=
45     (1-eta)*((Fhat (1,v)).1-‖(Fhat (1,v)).2‖)+eta*g
46   rw [smul_zero,add_zero,norm_smul,Real.norm_eq_abs,abs_of_nonneg (sub_nonneg.mpr heta1)]
47   ring
48 
49 theorem estimate_slack_lower (Fstar Fhat : State V →L[ℝ] State V) (d : ℝ)
50     (hstar : ∀ z∈cone,Fstar z∈cone)
51     (herror : ∀ v : V,‖v‖≤1 → |((Fhat-Fstar) (1,v)).1|+‖((Fhat-Fstar) (1,v)).2‖≤d)
52     (v : V) (hv : ‖v‖≤1) : -d≤slack (Fhat (1,v)) := by
53   have hp : 0≤slack (Fstar (1,v)) := sub_nonneg.mpr (hstar (1,v) hv)
54   have he := herror v hv
55   have ha := slack_add_lower (Fstar (1,v)) ((Fhat-Fstar) (1,v))
56   have hid : Fstar (1,v)+(Fhat-Fstar) (1,v)=Fhat (1,v) := by
57     simp only [sub_apply]
58     abel
59   rw [hid] at ha
60   linarith
61 
62 variable [FiniteDimensional ℝ V]
63 
64 /-- The actual repaired minimum has the exact P73 lower bound. -/
65 theorem repair_margin (Fstar Fhat : State V →L[ℝ] State V) (d g eta : ℝ)
66     (heta1 : eta≤1) (hstar : ∀ z∈cone,Fstar z∈cone)
67     (herror : ∀ v : V,‖v‖≤1 → |((Fhat-Fstar) (1,v)).1|+‖((Fhat-Fstar) (1,v)).2‖≤d) :
68     eta*g-(1-eta)*d≤sigma (repair Fhat g eta) := by
69   apply (le_sigma_iff _ _).mpr
70   intro v hv
71   rw [repair_slack Fhat g eta heta1]
72   have h := mul_le_mul_of_nonneg_left (estimate_slack_lower Fstar Fhat d hstar herror v hv)
73     (sub_nonneg.mpr heta1)
74   nlinarith
75 
76 /-- An extra combined output uncertainty is charged against the repaired slack. -/
77 theorem robust_repair_preserves (Fstar Fhat Delta : State V →L[ℝ] State V)
78     (d g eta nu : ℝ) (heta1 : eta≤1) (hstar : ∀ z∈cone,Fstar z∈cone)
79     (herror : ∀ v : V,‖v‖≤1 → |((Fhat-Fstar) (1,v)).1|+‖((Fhat-Fstar) (1,v)).2‖≤d)
80     (hnu : ∀ v : V,‖v‖≤1 → |(Delta (1,v)).1|+‖(Delta (1,v)).2‖≤nu)
81     (hcover : (1-eta)*d+nu≤eta*g) {z : State V} (hz : z∈cone) :
82     (repair Fhat g eta+Delta) z∈cone := by
83   apply preserves_of_normalized _ _ hz
84   intro v hv
85   have hm := (repair_margin Fstar Fhat d g eta heta1 hstar herror).trans
86     (sigma_le (repair Fhat g eta) v hv)
87   have he := hnu v hv
88   have ha := slack_add_lower (repair Fhat g eta (1,v)) (Delta (1,v))
89   have hs : 0≤slack (repair Fhat g eta (1,v)+Delta (1,v)) := by linarith
90   unfold slack at hs
91   change ‖(repair Fhat g eta (1,v)+Delta (1,v)).2‖≤(repair Fhat g eta (1,v)+Delta (1,v)).1
92   exact sub_nonneg.mp hs
93 
94 /-- Raw estimates retain exact integrated mass without presuming cone positivity. -/
95 structure EstimateFamily where
96   op : A → ℝ → State V →L[ℝ] State V
97   measurable_op : ∀ a,Measurable (op a)
98   integrable_op : ∀ a,Integrable (op a) UniformIntervalMoments.measure
99   mass_preserving : ∀ a z,probabilityCone.mass ((∫ u,op a u∂UniformIntervalMoments.measure) z)=probabilityCone.mass z
100 
101 /-- The declared strictly positive normalized scalar reset density. -/
102 structure ResetProfile where
103   density : A → ℝ → ℝ
104   measurable_density : ∀ a,Measurable (density a)
105   integrable_density : ∀ a,Integrable (density a) UniformIntervalMoments.measure
106   minimum : ℝ
107   minimum_positive : 0<minimum
108   lower : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → minimum≤density a u
109   integral_one : ∀ a,(∫ u,density a u∂UniformIntervalMoments.measure)=1
110 
111 variable [MeasurableSpace V] [BorelSpace V]
112 
113 /-- The reference instrument has exactly the declared reset density and center state. -/
114 noncomputable def ResetProfile.instrument (g : ResetProfile (A := A)) :
115     DensityInstrument (A := A) (probabilityCone (V := V)) UniformIntervalMoments.measure where
116   op a u := resetOperator (g.density a u)
117   measurable_op a := (g.measurable_density a).smul measurable_const
118   integrable_op a := (g.integrable_density a).smul_const (centerReset (V := V))
119   positive a := by
120     filter_upwards [PolynomialGram.uniform_ae_interval] with u hu
121     intro z hz
122     exact resetOperator_positive _ (g.minimum_positive.le.trans (g.lower a u hu)) hz
123   mass_preserving a z := by
124     change probabilityCone.mass ((∫ u,g.density a u • (centerReset (V := V))∂UniformIntervalMoments.measure) z)=_
125     rw [integral_smul_const,g.integral_one,one_smul]
126     exact centerReset_mass z
127 
128 /-- Mixing keeps the estimate's exact integrated mass even before proving positivity. -/
129 noncomputable def mixedFamily (H : EstimateFamily (V := V) (A := A))
130     (g : ResetProfile (A := A)) (eta : ℝ) : EstimateFamily (V := V) (A := A) where
131   op a u := repair (H.op a u) (g.density a u) eta
132   measurable_op a := ((H.measurable_op a).const_smul (1-eta)).add
133     (((g.instrument (V := V)).measurable_op a).const_smul eta)
134   integrable_op a := ((H.integrable_op a).smul (1-eta)).add
135     (((g.instrument (V := V)).integrable_op a).smul eta)
136   mass_preserving a z := by
137     change probabilityCone.mass ((∫ u,(1-eta) • H.op a u+eta • (g.instrument (V := V)).op a u
138       ∂UniformIntervalMoments.measure) z)=_
139     have hH : Integrable (fun u => (1-eta) • H.op a u) UniformIntervalMoments.measure :=
140       (H.integrable_op a).smul (1-eta)
141     have hN : Integrable (fun u => eta • (g.instrument (V := V)).op a u) UniformIntervalMoments.measure :=
142       ((g.instrument (V := V)).integrable_op a).smul eta
143     rw [integral_add hH hN,integral_smul,integral_smul]
144     simp only [add_apply,smul_apply,map_add,map_smul,smul_eq_mul,H.mass_preserving,
145       (g.instrument (V := V)).mass_preserving]
146     ring
147 
148 /-- A full interval repair witness constructs a true model; positivity is derived. -/
149 noncomputable def repairedInstrument (D : DensityInstrument (A := A) (probabilityCone (V := V)) UniformIntervalMoments.measure)
150     (H : EstimateFamily (V := V) (A := A)) (g : ResetProfile (A := A))
151     (eta : ℝ) (heta1 : eta≤1) (d : A → ℝ → ℝ)
152     (hstar : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ z∈cone,D.op a u z∈cone)
153     (herror : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → ∀ v : V,‖v‖≤1 →
154       |((H.op a u-D.op a u) (1,v)).1|+‖((H.op a u-D.op a u) (1,v)).2‖≤d a u)
155     (hcover : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → (1-eta)*d a u≤eta*g.density a u) :
156     DensityInstrument (A := A) (probabilityCone (V := V)) UniformIntervalMoments.measure where
157   op := (mixedFamily H g eta).op
158   measurable_op := (mixedFamily H g eta).measurable_op
159   integrable_op := (mixedFamily H g eta).integrable_op
160   mass_preserving := (mixedFamily H g eta).mass_preserving
161   positive a := by
162     filter_upwards [PolynomialGram.uniform_ae_interval] with u hu
163     intro z hz
164     change repair (H.op a u) (g.density a u) eta z∈cone
165     have hr := robust_repair_preserves (D.op a u) (H.op a u) 0 (d a u) (g.density a u)
166       eta 0 heta1 (hstar a u hu) (herror a u hu) (fun _ _ => by simp) (by simpa using hcover a u hu) hz
167     simpa only [add_zero] using hr
168 
169 /-- Polynomial estimates acquire measurability, Bochner integrability and exact mass from their actual coefficients. -/
170 noncomputable def EstimateFamily.ofPolynomial {n : ℕ}
171     (B : A → Fin n → State V →L[ℝ] State V)
172     (hm : ∀ a z,probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • B a k) z)=probabilityCone.mass z) :
173     EstimateFamily (V := V) (A := A) where
174   op a := PolynomialGram.operatorPolynomial (B a)
175   measurable_op a := (PolynomialGram.operatorPolynomial_continuous _).measurable
176   integrable_op a := PolynomialGram.operatorPolynomial_integrable _
177   mass_preserving a z := by rw [PolynomialGram.operatorPolynomial_integral]; exact hm a z
178 
179 /-- A genuine finite scalar polynomial reset profile, normalized by exact power moments. -/
180 noncomputable def ResetProfile.ofPolynomial {n : ℕ} (c : A → Fin n → ℝ)
181     (gmin : ℝ) (hgmin : 0<gmin)
182     (hlower : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → gmin≤(Polynomial.ofFn n (c a)).eval u)
183     (hm : ∀ a,∑ k : Fin n,c a k*UniformIntervalMoments.moment k=1) : ResetProfile (A := A) where
184   density a u := (Polynomial.ofFn n (c a)).eval u
185   measurable_density a := (Polynomial.continuous _).measurable
186   integrable_density a := UniformIntervalMoments.continuous_integrable (Polynomial.continuous _)
187   minimum := gmin
188   minimum_positive := hgmin
189   lower := hlower
190   integral_one a := by
191     simp_rw [UniformIntervalMoments.eval_ofFn]
192     rw [UniformIntervalMoments.integral_power_sum]
193     exact hm a
194 
195 omit [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] in
196 theorem EstimateFamily.applied_integrable (H : EstimateFamily (V := V) (A := A)) (a : A) (z : State V) :
197     Integrable (fun u => H.op a u z) UniformIntervalMoments.measure :=
198   (ContinuousLinearMap.apply ℝ (State V) z).integrable_comp (H.integrable_op a)
199 
200 omit [MeasurableSpace V] [BorelSpace V] in
201 /-- The reset's comparison cost is integrated: point densities are not bounded by one. -/
202 theorem ResetProfile.integrated_cost_le_two (g : ResetProfile (A := A))
203     (D : DensityInstrument (A := A) (probabilityCone (V := V)) UniformIntervalMoments.measure)
204     (a : A) (z : State V) (hz : z∈probabilityCone.base) :
205     (∫ u,probabilityCone.value ((g.instrument (V := V)).op a u z-D.op a u z)∂UniformIntervalMoments.measure)≤2 := by
206   have hi := probabilityCone.integrable_value
207     (((g.instrument (V := V)).applied_integrable a z).sub (D.applied_integrable a z))
208   have hj := ((g.instrument (V := V)).density_integrable a z).add (D.density_integrable a z)
209   have hp : ∀ᵐ u∂UniformIntervalMoments.measure,
210       probabilityCone.value ((g.instrument (V := V)).op a u z-D.op a u z)≤
211         (g.instrument (V := V)).density a u z+D.density a u z := by
212     filter_upwards [(g.instrument (V := V)).positive a,D.positive a] with u hN hD
213     exact (probabilityCone.value_sub_le _ _).trans_eq (by
214       rw [probabilityCone.value_on_cone (hN z hz.1),probabilityCone.value_on_cone (hD z hz.1)]
215       rfl)
216   calc
217     _≤∫ u,(g.instrument (V := V)).density a u z+D.density a u z∂UniformIntervalMoments.measure :=
218       integral_mono_ae hi hj hp
219     _=2 := by
220       rw [integral_add ((g.instrument (V := V)).density_integrable a z) (D.density_integrable a z),
221         (g.instrument (V := V)).integral_density,D.integral_density,hz.2]
222       norm_num
223 
224 omit [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] in
225 theorem repair_difference (Fhat Fstar : State V →L[ℝ] State V) (g eta : ℝ) (z : State V) :
226     repair Fhat g eta z-Fstar z=(1-eta) • (Fhat z-Fstar z)+eta • (resetOperator g z-Fstar z) := by
227   simp only [repair,add_apply,smul_apply,smul_sub]
228   module
229 
230 omit [MeasurableSpace V] [BorelSpace V] in
231 /-- The repair charge 2 eta is retained separately from the estimate error. -/
232 theorem repair_integrated_error
233     (D : DensityInstrument (A := A) (probabilityCone (V := V)) UniformIntervalMoments.measure)
234     (H : EstimateFamily (V := V) (A := A)) (g : ResetProfile (A := A))
235     (eta : ℝ) (heta0 : 0≤eta) (heta1 : eta≤1) (epsilon : ℝ) (a : A) (z : State V)
236     (hz : z∈probabilityCone.base)
237     (herror : (∫ u,probabilityCone.value (H.op a u z-D.op a u z)∂UniformIntervalMoments.measure)≤epsilon) :
238     (∫ u,probabilityCone.value (repair (H.op a u) (g.density a u) eta z-D.op a u z)
239       ∂UniformIntervalMoments.measure)≤(1-eta)*epsilon+2*eta := by
240   have hi := probabilityCone.integrable_value
241     (((mixedFamily H g eta).applied_integrable a z).sub (D.applied_integrable a z))
242   have hH : Integrable (fun u => probabilityCone.value (H.op a u z-D.op a u z)) UniformIntervalMoments.measure :=
243     probabilityCone.integrable_value ((H.applied_integrable a z).sub (D.applied_integrable a z))
244   have hN : Integrable (fun u => probabilityCone.value ((g.instrument (V := V)).op a u z-D.op a u z))
245       UniformIntervalMoments.measure := probabilityCone.integrable_value
246         (((g.instrument (V := V)).applied_integrable a z).sub (D.applied_integrable a z))
247   have hp (u : ℝ) : probabilityCone.value (repair (H.op a u) (g.density a u) eta z-D.op a u z)≤
248       (1-eta)*probabilityCone.value (H.op a u z-D.op a u z)+
249         eta*probabilityCone.value ((g.instrument (V := V)).op a u z-D.op a u z) := by
250     rw [repair_difference]
251     exact (probabilityCone.value_add_le _ _).trans_eq (by
252       rw [probabilityCone.value_smul_of_nonneg (sub_nonneg.mpr heta1),
253         probabilityCone.value_smul_of_nonneg heta0]
254       rfl)
255   calc
256     _≤∫ u,(1-eta)*probabilityCone.value (H.op a u z-D.op a u z)+
257         eta*probabilityCone.value ((g.instrument (V := V)).op a u z-D.op a u z)∂UniformIntervalMoments.measure :=
258       integral_mono hi ((hH.const_mul (1-eta)).add (hN.const_mul eta)) hp
259     _=(1-eta)*(∫ u,probabilityCone.value (H.op a u z-D.op a u z)∂UniformIntervalMoments.measure)+
260         eta*(∫ u,probabilityCone.value ((g.instrument (V := V)).op a u z-D.op a u z)∂UniformIntervalMoments.measure) := by
261       rw [integral_add (hH.const_mul (1-eta)) (hN.const_mul eta),integral_const_mul,integral_const_mul]
262     _≤(1-eta)*epsilon+2*eta := by
263       have hreset := mul_le_mul_of_nonneg_left (g.integrated_cost_le_two D a z hz) heta0
264       nlinarith [mul_le_mul_of_nonneg_left herror (sub_nonneg.mpr heta1)]
265 
266 /-- The actual complete common-policy laws satisfy P73's probability-convention TV budget. -/
267 theorem common_policy_law_error [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
268     (D G : DensityInstrument (A := A) (probabilityCone (V := V)) UniformIntervalMoments.measure)
269     (H : EstimateFamily (V := V) (A := A)) (g : ResetProfile (A := A))
270     (eta : ℝ) (heta0 : 0≤eta) (heta1 : eta≤1) (epsilon : ℝ)
271     (hG : ∀ a u,G.op a u=repair (H.op a u) (g.density a u) eta)
272     (herror : ∀ a z,z∈probabilityCone.base →
273       (∫ u,probabilityCone.value (H.op a u z-D.op a u z)∂UniformIntervalMoments.measure)≤epsilon)
274     (policy : ContinuousRecords.Policy (A := A) (Y := ℝ))
275     (z : DensityInstrument.State (probabilityCone (V := V))) (horizon : ℕ) :
276     SequentialLowerCertificate.lawTV (TimeRecords.recordLaw (fun _ => G) policy z.1 horizon)
277       (TimeRecords.recordLaw (fun _ => D) policy z.1 horizon)≤
278       min 1 (((horizon : ℝ)/2)*((1-eta)*epsilon+2*eta)) := by
279   have hb0 : 0≤(1-eta)*epsilon+2*eta := by
280     rcases isEmpty_or_nonempty A with hA | hA
281     · let := hA
282       have hc := policy.sum_one 0 PUnit.unit
283       simp at hc
284     · let := hA
285       let a : A := Classical.choice hA
286       have he0 : 0≤epsilon := (integral_nonneg (fun u => probabilityCone.value_nonneg _)).trans (herror a z.1 z.2)
287       exact add_nonneg (mul_nonneg (sub_nonneg.mpr heta1) he0) (mul_nonneg (by norm_num) heta0)
288   have hd : ∀ a w,w∈probabilityCone.base →
289       (∫ u,probabilityCone.value (G.op a u w-D.op a u w)∂UniformIntervalMoments.measure)≤(1-eta)*epsilon+2*eta := by
290     intro a w hw
291     simpa only [hG] using repair_integrated_error D H g eta heta0 heta1 epsilon a w hw (herror a w hw)
292   have ht := ContinuousTV.record_lawTV_le (fun _ => G) (fun _ => D) policy z z
293     (fun _ => (1-eta)*epsilon+2*eta) (fun _ => hb0) (fun _ a w hw => hd a w hw) 0 (by simp) horizon
294   convert ht using 1
295   congr 1
296   simp only [Finset.sum_const,Finset.card_range,nsmul_eq_mul,zero_add]
297   ring
298 
299 end Komorebi.LSM.InteriorRepair

Back to source controls