BernsteinCoefficientError.lean

1 import KomorebiLSM.PositivePolynomialApproximation
2 import KomorebiLSM.ContinuousRecords
3 
4 /-! P65: positive fitted Bernstein coefficients, genuine base-norm coefficient
5 error, approximation bias, and a separate correction budget. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.BernsteinCoefficientError
8 open MeasureTheory ContinuousInstrument
9 open scoped BigOperators
10 noncomputable section
11 
12 variable {E A : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
13   [FiniteDimensional ℝ E]
14 variable (C : BaseNorm.ProbabilityCone E)
15 
16 /-- The fitted density is the literal Bernstein combination of the fitted operators. -/
17 def combination (n : ℕ) (T : Fin (n+1) → E →L[ℝ] E) (x : ℝ) : E →L[ℝ] E :=
18   ∑ k : Fin (n+1),BernsteinKernel.basis n k x • T k
19 
20 omit [FiniteDimensional ℝ E] in
21 /-- Constant fitted coefficients give exactly the same constant density operator. -/
22 theorem combination_constant (n : ℕ) (T : E →L[ℝ] E) (x : ℝ) :
23     combination n (fun _ => T) x=T := by
24   unfold combination
25   rw [← Finset.sum_smul,BernsteinKernel.sum_basis,one_smul]
26 
27 omit [FiniteDimensional ℝ E] in
28 theorem combination_continuous (n : ℕ) (T : Fin (n+1) → E →L[ℝ] E) :
29     Continuous (combination n T) := by
30   exact continuous_finsetSum _ (fun k _ => (BernsteinKernel.basis_continuous n k).smul continuous_const)
31 
32 omit [FiniteDimensional ℝ E] in
33 theorem combination_integrable (n : ℕ) (T : Fin (n+1) → E →L[ℝ] E) :
34     Integrable (combination n T) BernsteinKernel.measure :=
35   BernsteinKernel.continuous_integrable (combination_continuous n T)
36 
37 /-- The coefficient average is the actual Bochner integral of the fitted density. -/
38 theorem combination_integral (n : ℕ) (T : Fin (n+1) → E →L[ℝ] E) :
39     (∫ x,combination n T x∂BernsteinKernel.measure)=
40       (1/((n : ℝ)+1)) • ∑ k,T k := by
41   change (∫ x,∑ k : Fin (n+1),BernsteinKernel.basis n k x • T k∂BernsteinKernel.measure)=_
42   rw [integral_finsetSum]
43   · simp_rw [integral_smul_const,BernsteinKernel.basis_integral]
44     rw [Finset.smul_sum]
45   · intro k _
46     exact BernsteinKernel.continuous_integrable
47       ((BernsteinKernel.basis_continuous n k).smul continuous_const)
48 
49 omit [FiniteDimensional ℝ E] in
50 /-- Nonnegative Bernstein weights preserve the same actual cone pointwise. -/
51 theorem combination_positive (n : ℕ) (T : Fin (n+1) → E →L[ℝ] E)
52     (hT : ∀ k z,z∈C.carrier → T k z∈C.carrier)
53     (x : ℝ) (hx : x∈Set.Icc (0 : ℝ) 1) (z : E) (hz : z∈C.carrier) :
54     combination n T x z∈C.carrier := by
55   simp only [combination,sum_apply,smul_apply]
56   change (∑ k : Fin (n+1),BernsteinKernel.basis n k x • T k z)∈C.carrier
57   apply Finset.sum_induction
58   · intro a b ha hb
59     exact C.add_mem ha hb
60   · exact C.zero_mem
61   · intro k _
62     exact C.smul_mem (BernsteinKernel.basis_nonneg n k hx) (hT k z hz)
63 
64 variable [MeasurableSpace E] [BorelSpace E]
65 
66 /-- Positivity and exact average mass construct a true density instrument. -/
67 def fittedInstrument (n : ℕ) (T : A → Fin (n+1) → E →L[ℝ] E)
68     (hT : ∀ a k z,z∈C.carrier → T a k z∈C.carrier)
69     (hm : ∀ a z,C.mass (((1/((n : ℝ)+1)) • ∑ k,T a k) z)=C.mass z) :
70     DensityInstrument (A := A) C BernsteinKernel.measure where
71   op a := combination n (T a)
72   measurable_op a := (combination_continuous n (T a)).measurable
73   integrable_op a := combination_integrable n (T a)
74   positive a := BernsteinKernel.support_ae.mono (fun x hx z hz => combination_positive C n (T a) (hT a) x hx z hz)
75   mass_preserving a z := by rw [combination_integral]; exact hm a z
76 
77 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
78 /-- The finite coefficient premise bounds the actual positive-decomposition infimum. -/
79 theorem coefficient_error_point (n : ℕ) (T U : Fin (n+1) → E →L[ℝ] E)
80     (eta : Fin (n+1) → ℝ) (z : E)
81     (herror : ∀ k,C.value (T k z-U k z)≤eta k)
82     (x : ℝ) (hx : x∈Set.Icc (0 : ℝ) 1) :
83     C.value (combination n T x z-combination n U x z)≤
84       ∑ k : Fin (n+1),BernsteinKernel.basis n k x*eta k := by
85   have he : combination n T x z-combination n U x z=
86       ∑ k : Fin (n+1),BernsteinKernel.basis n k x • (T k z-U k z) := by
87     simp only [combination,sum_apply,smul_apply,
88       smul_sub,Finset.sum_sub_distrib]
89   rw [he]
90   calc
91     _≤∑ k : Fin (n+1),C.value (BernsteinKernel.basis n k x • (T k z-U k z)) := C.value_sum_le _ _
92     _=∑ k : Fin (n+1),BernsteinKernel.basis n k x*C.value (T k z-U k z) := by
93       apply Finset.sum_congr rfl
94       intro k _
95       exact C.value_smul_of_nonneg (BernsteinKernel.basis_nonneg n k hx) _
96     _≤_ := Finset.sum_le_sum (fun k _ => mul_le_mul_of_nonneg_left (herror k)
97       (BernsteinKernel.basis_nonneg n k hx))
98 
99 omit [MeasurableSpace E] [BorelSpace E] in
100 /-- Integration yields exactly the arithmetic mean of the coefficient error budgets. -/
101 theorem coefficient_integrated_error (n : ℕ) (T U : Fin (n+1) → E →L[ℝ] E)
102     (eta : Fin (n+1) → ℝ) (z : E) (herror : ∀ k,C.value (T k z-U k z)≤eta k) :
103     (∫ x,C.value (combination n T x z-combination n U x z)∂BernsteinKernel.measure)≤
104       (1/((n : ℝ)+1))*∑ k,eta k := by
105   have hi := C.integrable_value
106     (((ContinuousLinearMap.apply ℝ E z).integrable_comp (combination_integrable n T)).sub
107       ((ContinuousLinearMap.apply ℝ E z).integrable_comp (combination_integrable n U)))
108   have hj : Integrable (fun x => ∑ k : Fin (n+1),BernsteinKernel.basis n k x*eta k)
109       BernsteinKernel.measure :=
110     BernsteinKernel.continuous_integrable (continuous_finsetSum _
111       (fun k _ => (BernsteinKernel.basis_continuous n k).mul continuous_const))
112   calc
113     _≤∫ x,∑ k : Fin (n+1),BernsteinKernel.basis n k x*eta k∂BernsteinKernel.measure := by
114       apply integral_mono_ae hi hj
115       exact BernsteinKernel.support_ae.mono (fun x hx => coefficient_error_point C n T U eta z herror x hx)
116     _=∑ k : Fin (n+1),(1/((n : ℝ)+1))*eta k := by
117       rw [integral_finsetSum]
118       · simp_rw [integral_mul_const,BernsteinKernel.basis_integral]
119       · intro k _
120         exact BernsteinKernel.continuous_integrable ((BernsteinKernel.basis_continuous n k).mul continuous_const)
121     _=_ := (Finset.mul_sum _ _ _).symm
122 
123 omit [MeasurableSpace E] [BorelSpace E] in
124 /-- Triangle inequality for literal integrated base-norm discrepancies. -/
125 theorem integrated_triangle (F G H : ℝ → E →L[ℝ] E)
126     (hF : Integrable F BernsteinKernel.measure) (hG : Integrable G BernsteinKernel.measure)
127     (hH : Integrable H BernsteinKernel.measure) (z : E) :
128     (∫ x,C.value (F x z-H x z)∂BernsteinKernel.measure)≤
129       (∫ x,C.value (F x z-G x z)∂BernsteinKernel.measure)+
130         ∫ x,C.value (G x z-H x z)∂BernsteinKernel.measure := by
131   have hFV := (ContinuousLinearMap.apply ℝ E z).integrable_comp hF
132   have hGV := (ContinuousLinearMap.apply ℝ E z).integrable_comp hG
133   have hHV := (ContinuousLinearMap.apply ℝ E z).integrable_comp hH
134   have hFG : Integrable (fun x => C.value (F x z-G x z)) BernsteinKernel.measure :=
135     C.integrable_value (hFV.sub hGV)
136   have hGH : Integrable (fun x => C.value (G x z-H x z)) BernsteinKernel.measure :=
137     C.integrable_value (hGV.sub hHV)
138   calc
139     _≤∫ x,C.value (F x z-G x z)+C.value (G x z-H x z)∂BernsteinKernel.measure := by
140       apply integral_mono (C.integrable_value (hFV.sub hHV)) (hFG.add hGH)
141       intro x
142       change C.value (F x z-H x z)≤C.value (F x z-G x z)+C.value (G x z-H x z)
143       have he : F x z-H x z=(F x z-G x z)+(G x z-H x z) := by abel
144       rw [he]
145       exact C.value_add_le _ _
146     _=_ := integral_add hFG hGH
147 
148 /-- The finite action maximum is taken over the actual coefficient mean budgets. -/
149 def maximumCoefficientError [Fintype A] (n : ℕ) (eta : A → Fin (n+1) → ℝ) : ℝ :=
150   sSup (Set.range (fun a => (1/((n : ℝ)+1))*∑ k,eta a k))
151 
152 theorem coefficient_error_le_maximum [Fintype A] (n : ℕ) (eta : A → Fin (n+1) → ℝ) (a : A) :
153     (1/((n : ℝ)+1))*∑ k,eta a k≤maximumCoefficientError n eta :=
154   le_csSup (Set.finite_range _).bddAbove (Set.mem_range_self a)
155 
156 omit [MeasurableSpace E] [BorelSpace E] in
157 /-- Genuine approximation bias and coefficient error remain separate addends. -/
158 theorem bias_plus_coefficient_error (n : ℕ)
159     (D : DensityInstrument (A := A) C BernsteinKernel.measure)
160     (T : A → Fin (n+1) → E →L[ℝ] E) (eta : A → Fin (n+1) → ℝ)
161     (L : ℝ) (hL : 0≤L)
162     (hLip : ∀ a x,x∈Set.Icc (0 : ℝ) 1 → ∀ v∈Set.Icc (0 : ℝ) 1,
163       PositiveCellApproximation.inducedNorm (C := C) (D.op a v-D.op a x)≤L*|v-x|)
164     (herror : ∀ a k z,z∈C.base →
165       C.value (PositivePolynomialApproximation.coefficient n (D.op a) k z-T a k z)≤eta a k)
166     (a : A) (z : E) (hz : z∈C.base) :
167     (∫ x,C.value (D.op a x z-combination n (T a) x z)∂BernsteinKernel.measure)≤
168       L/Real.sqrt (3*((n : ℝ)+2))+(1/((n : ℝ)+1))*∑ k,eta a k := by
169   have htriangle := integrated_triangle C (D.op a)
170     (PositivePolynomialApproximation.approximation n (D.op a)) (combination n (T a))
171     (D.integrable_op a) (PositivePolynomialApproximation.approximation_integrable n (D.op a))
172     (combination_integrable n (T a)) z
173   have hbias := PositivePolynomialApproximation.approximating_instrument_discrepancy
174     n D L hL hLip a z hz
175   have hcoef := coefficient_integrated_error C n
176     (PositivePolynomialApproximation.coefficient n (D.op a)) (T a) (eta a) z
177     (fun k => herror a k z hz)
178   exact htriangle.trans (add_le_add hbias hcoef)
179 
180 omit [MeasurableSpace E] [BorelSpace E] in
181 /-- The stated action-uniform budget uses the actual finite maximum. -/
182 theorem uniform_bias_plus_coefficient_error [Fintype A] (n : ℕ)
183     (D : DensityInstrument (A := A) C BernsteinKernel.measure)
184     (T : A → Fin (n+1) → E →L[ℝ] E) (eta : A → Fin (n+1) → ℝ)
185     (L : ℝ) (hL : 0≤L)
186     (hLip : ∀ a x,x∈Set.Icc (0 : ℝ) 1 → ∀ v∈Set.Icc (0 : ℝ) 1,
187       PositiveCellApproximation.inducedNorm (C := C) (D.op a v-D.op a x)≤L*|v-x|)
188     (herror : ∀ a k z,z∈C.base →
189       C.value (PositivePolynomialApproximation.coefficient n (D.op a) k z-T a k z)≤eta a k)
190     (a : A) (z : E) (hz : z∈C.base) :
191     (∫ x,C.value (D.op a x z-combination n (T a) x z)∂BernsteinKernel.measure)≤
192       L/Real.sqrt (3*((n : ℝ)+2))+maximumCoefficientError n eta :=
193   (bias_plus_coefficient_error C n D T eta L hL hLip herror a z hz).trans
194     (add_le_add le_rfl (coefficient_error_le_maximum n eta a))
195 
196 omit [MeasurableSpace E] [BorelSpace E] in
197 /-- A separately known model-correction discrepancy adds by another actual triangle inequality. -/
198 theorem separate_correction_budget [Fintype A] (n : ℕ)
199     (D G : DensityInstrument (A := A) C BernsteinKernel.measure)
200     (T : A → Fin (n+1) → E →L[ℝ] E) (eta : A → Fin (n+1) → ℝ)
201     (L correction : ℝ) (hL : 0≤L)
202     (hLip : ∀ a x,x∈Set.Icc (0 : ℝ) 1 → ∀ v∈Set.Icc (0 : ℝ) 1,
203       PositiveCellApproximation.inducedNorm (C := C) (D.op a v-D.op a x)≤L*|v-x|)
204     (herror : ∀ a k z,z∈C.base →
205       C.value (PositivePolynomialApproximation.coefficient n (D.op a) k z-T a k z)≤eta a k)
206     (hcorrection : ∀ a z,z∈C.base →
207       (∫ x,C.value (combination n (T a) x z-G.op a x z)∂BernsteinKernel.measure)≤correction)
208     (a : A) (z : E) (hz : z∈C.base) :
209     (∫ x,C.value (D.op a x z-G.op a x z)∂BernsteinKernel.measure)≤
210       L/Real.sqrt (3*((n : ℝ)+2))+maximumCoefficientError n eta+correction :=
211   (integrated_triangle C (D.op a) (combination n (T a)) (G.op a)
212     (D.integrable_op a) (combination_integrable n (T a)) (G.integrable_op a) z).trans
213       (add_le_add (uniform_bias_plus_coefficient_error C n D T eta L hL hLip herror a z hz)
214         (hcorrection a z hz))
215 
216 /-- Every finite joint record law of the fitted valid model is normalized. -/
217 theorem fitted_record_probability [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
218     (n : ℕ) (T : A → Fin (n+1) → E →L[ℝ] E)
219     (hT : ∀ a k z,z∈C.carrier → T a k z∈C.carrier)
220     (hm : ∀ a z,C.mass (((1/((n : ℝ)+1)) • ∑ k,T a k) z)=C.mass z)
221     (policy : ContinuousRecords.Policy (A := A) (Y := ℝ))
222     (z : E) (hz : z∈C.base) (horizon : ℕ) :
223     IsProbabilityMeasure (ContinuousRecords.recordLaw (fittedInstrument C n T hT hm) policy z horizon) :=
224   ContinuousRecords.recordLaw_probability (fittedInstrument C n T hT hm) policy ⟨z,hz⟩ horizon
225 
226 end
227 end Komorebi.LSM.BernsteinCoefficientError

Back to source controls