CoefficientBox3.lean

1 import KomorebiLSM.RobustOrientedMargin
2 
3 /-! P76's literal three-coordinate polynomial coefficient box. The spatial
4 norm is Euclidean, and integrated mass remains a separate affine constraint. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.CoefficientBox3
7 open scoped BigOperators Matrix
8 open LorentzCylinder RobustOrientedMargin
9 
10 abbrev Spatial := EuclideanSpace ℝ (Fin 2)
11 abbrev State := LorentzCylinder.State Spatial
12 abbrev Index := Unit ⊕ Fin 2
13 abbrev Coefficient := Matrix Index Index ℝ
14 
15 /-- Mass first, followed by the two actual Euclidean spatial coordinates. -/
16 def coordinates : State ≃ₗ[ℝ] (Index → ℝ) where
17   toFun z := Sum.elim (fun _ => z.1) (fun i => z.2 i)
18   invFun x := (x (.inl ()), WithLp.toLp 2 (fun i => x (.inr i)))
19   left_inv z := by apply Prod.ext <;> rfl
20   right_inv x := by funext i; cases i <;> rfl
21   map_add' x y := by funext i; cases i <;> rfl
22   map_smul' a x := by funext i; cases i <;> rfl
23 
24 /-- Literal matrix multiplication expressed in the Lorentz state space. -/
25 noncomputable def operator (E : Coefficient) : State →L[ℝ] State :=
26   ((coordinates.symm.toLinearMap.comp E.toLin').comp coordinates.toLinearMap).toContinuousLinearMap
27 
28 @[simp] theorem operator_one_apply (z : State) : operator (1 : Coefficient) z=z := by
29   change coordinates.symm ((1 : Coefficient) *ᵥ coordinates z)=z
30   rw [Matrix.one_mulVec,LinearEquiv.symm_apply_apply]
31 
32 @[simp] theorem coordinates_operator (E : Coefficient) (z : State) (i : Index) :
33     coordinates (operator E z) i=∑ j : Index,E i j*coordinates z j := by
34   change coordinates (coordinates.symm (E *ᵥ coordinates z)) i= _
35   rw [LinearEquiv.apply_symm_apply]
36   rfl
37 
38 theorem normalized_coordinate_bound (v : Spatial) (hv : ‖v‖≤1) (j : Index) :
39     |coordinates (1,v) j|≤1 := by
40   cases j with
41   | inl j => simp [coordinates]
42   | inr j =>
43     change |v j|≤1
44     have hcoord : |v j|≤‖v‖ := by simpa only [Real.norm_eq_abs] using PiLp.norm_apply_le v j
45     exact hcoord.trans hv
46 
47 theorem scalar_coefficient_bound (E : Coefficient) (r : ℝ)
48     (hE : ∀ i j,|E i j|≤r) (v : Spatial) (hv : ‖v‖≤1) (i : Index) :
49     |coordinates (operator E (1,v)) i|≤3*r := by
50   have hr : 0≤r := (abs_nonneg (E (.inl ()) (.inl ()))).trans (hE _ _)
51   rw [coordinates_operator]
52   calc
53     _ ≤ ∑ j : Index,|E i j*coordinates (1,v) j| := Finset.abs_sum_le_sum_abs _ _
54     _ ≤ ∑ _j : Index,r := by
55       apply Finset.sum_le_sum
56       intro j _
57       rw [abs_mul]
58       exact (mul_le_mul (hE i j) (normalized_coordinate_bound v hv j) (abs_nonneg _) hr).trans_eq (mul_one _)
59     _ = 3*r := by simp [Index]
60 
61 /-- The actual two-dimensional Euclidean norm is bounded by the L1 sum. -/
62 theorem spatial_norm_le_sum (v : Spatial) : ‖v‖≤|v 0|+|v 1| := by
63   have hs := EuclideanSpace.real_norm_sq_eq v
64   simp only [Fin.sum_univ_two] at hs
65   nlinarith [sq_abs (v 0),sq_abs (v 1),mul_nonneg (abs_nonneg (v 0)) (abs_nonneg (v 1)),
66     norm_nonneg v,abs_nonneg (v 0),abs_nonneg (v 1)]
67 
68 theorem coefficient_output_bounds (E : Coefficient) (r : ℝ)
69     (hE : ∀ i j,|E i j|≤r) (v : Spatial) (hv : ‖v‖≤1) :
70     |(operator E (1,v)).1|≤3*r ∧ ‖(operator E (1,v)).2‖≤6*r := by
71   have hm := scalar_coefficient_bound E r hE v hv (.inl ())
72   have h0 := scalar_coefficient_bound E r hE v hv (.inr 0)
73   have h1 := scalar_coefficient_bound E r hE v hv (.inr 1)
74   refine ⟨hm,?_⟩
75   have hb := spatial_norm_le_sum (operator E (1,v)).2
76   change |(operator E (1,v)).2 0|≤3*r at h0
77   change |(operator E (1,v)).2 1|≤3*r at h1
78   linarith
79 
80 theorem polynomial_mass {n : ℕ} (E : Fin n → Coefficient) (u : ℝ) (z : State) :
81     (PolynomialGram.operatorPolynomial (fun k => operator (E k)) u z).1=
82       ∑ k : Fin n,u^(k : ℕ)*(operator (E k) z).1 := by
83   change (LinearMap.fst ℝ ℝ Spatial) ((∑ k : Fin n,u^(k : ℕ) • operator (E k)) z)= _
84   simp only [sum_apply,smul_apply,map_sum,map_smul]
85   rfl
86 
87 theorem polynomial_spatial {n : ℕ} (E : Fin n → Coefficient) (u : ℝ) (z : State) :
88     (PolynomialGram.operatorPolynomial (fun k => operator (E k)) u z).2=
89       ∑ k : Fin n,u^(k : ℕ) • (operator (E k) z).2 := by
90   change (LinearMap.snd ℝ ℝ Spatial) ((∑ k : Fin n,u^(k : ℕ) • operator (E k)) z)= _
91   simp only [sum_apply,smul_apply,map_sum,map_smul]
92   rfl
93 
94 /-- Every entry budget controls the entire observation interval, not a grid. -/
95 theorem polynomial_output_bounds {n : ℕ} (E : Fin n → Coefficient) (r : Fin n → ℝ)
96     (hE : ∀ k i j,|E k i j|≤r k) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1)
97     (v : Spatial) (hv : ‖v‖≤1) :
98     |(PolynomialGram.operatorPolynomial (fun k => operator (E k)) u (1,v)).1|≤3*∑ k,r k ∧
99     ‖(PolynomialGram.operatorPolynomial (fun k => operator (E k)) u (1,v)).2‖≤6*∑ k,r k := by
100   have hr (k : Fin n) : 0≤r k := (abs_nonneg (E k (.inl ()) (.inl ()))).trans (hE k _ _)
101   have hp (k : Fin n) : |u^(k : ℕ)|≤1 := by
102     rw [abs_pow]
103     exact pow_le_one₀ (abs_nonneg _) (abs_le.mpr hu)
104   constructor
105   · rw [polynomial_mass]
106     calc
107       _ ≤ ∑ k : Fin n,|u^(k : ℕ)*(operator (E k) (1,v)).1| := Finset.abs_sum_le_sum_abs _ _
108       _ ≤ ∑ k : Fin n,3*r k := by
109         apply Finset.sum_le_sum
110         intro k _
111         rw [abs_mul]
112         exact (mul_le_mul (hp k) (coefficient_output_bounds (E k) (r k) (hE k) v hv).1
113           (abs_nonneg _) (by norm_num)).trans_eq (one_mul _)
114       _ = _ := (Finset.mul_sum _ _ _).symm
115   · rw [polynomial_spatial]
116     calc
117       _ ≤ ∑ k : Fin n,‖u^(k : ℕ) • (operator (E k) (1,v)).2‖ := norm_sum_le _ _
118       _ ≤ ∑ k : Fin n,6*r k := by
119         apply Finset.sum_le_sum
120         intro k _
121         rw [norm_smul,Real.norm_eq_abs]
122         exact (mul_le_mul (hp k) (coefficient_output_bounds (E k) (r k) (hE k) v hv).2
123           (norm_nonneg _) (by norm_num)).trans_eq (one_mul _)
124       _ = _ := (Finset.mul_sum _ _ _).symm
125 
126 /-- The submitted margin is consumed by the real P71 robustness theorem. -/
127 theorem coefficient_box_preserves {n : ℕ} (F : State →L[ℝ] State)
128     (E : Fin n → Coefficient) (r : Fin n → ℝ)
129     (hE : ∀ k i j,|E k i j|≤r k) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1)
130     (kappa : ℝ) (hmargin : kappa≤sigma F) (hcover : 9*(∑ k,r k)≤kappa)
131     {z : State} (hz : z∈cone) :
132     (F+PolynomialGram.operatorPolynomial (fun k => operator (E k)) u) z∈cone := by
133   apply robust_preserves F _ kappa (3*∑ k,r k) (6*∑ k,r k) hmargin
134     (fun v hv => (polynomial_output_bounds E r hE u hu v hv).1)
135     (fun v hv => (polynomial_output_bounds E r hE u hu v hv).2) _ hz
136   linarith
137 
138 /-- All coefficient entries, actions and interval values are covered by the
139 same submitted radii; the P71 certificate is constructed from those bounds. -/
140 theorem boxCertificate {A : Type*} {n : ℕ}
141     (F : A → Fin n → State →L[ℝ] State) (E : A → Fin n → Coefficient)
142     (r : Fin n → ℝ) (kappa : A → ℝ → ℝ)
143     (hE : ∀ a k i j,|E a k i j|≤r k)
144     (hmargin : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → kappa a u≤sigma (PolynomialGram.operatorPolynomial (F a) u))
145     (hcover : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → 9*(∑ k,r k)≤kappa a u) :
146     MarginCertificate F (fun a k => operator (E a k)) kappa
147       (fun _ _ => 3*∑ k,r k) (fun _ _ => 6*∑ k,r k) where
148   margin := hmargin
149   mass_error a u hu v hv := (polynomial_output_bounds (E a) r (hE a) u hu v hv).1
150   spatial_error a u hu v hv := (polynomial_output_bounds (E a) r (hE a) u hu v hv).2
151   cover a u hu := by linarith [hcover a u hu]
152 
153 /-- Exact mass is retained only for errors satisfying the literal integrated
154 mass-row-zero condition; it is not inferred from entry radii. -/
155 theorem exact_mass_with_error {A : Type*} {n : ℕ}
156     (F : A → Fin n → State →L[ℝ] State) (E : A → Fin n → Coefficient)
157     (hF : ∀ a z,probabilityCone.mass ((∫ u,PolynomialGram.operatorPolynomial (F a) u
158       ∂UniformIntervalMoments.measure) z)=probabilityCone.mass z)
159     (hE : ∀ a z,probabilityCone.mass ((∫ u,PolynomialGram.operatorPolynomial (fun k => operator (E a k)) u
160       ∂UniformIntervalMoments.measure) z)=0) (a : A) (z : State) :
161     probabilityCone.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • (F a k+operator (E a k))) z)=
162       probabilityCone.mass z := by
163   simp only [PolynomialGram.operatorPolynomial_integral] at hF hE
164   rw [show (∑ k : Fin n,UniformIntervalMoments.moment k • (F a k+operator (E a k)))=
165       (∑ k : Fin n,UniformIntervalMoments.moment k • F a k)+
166         ∑ k : Fin n,UniformIntervalMoments.moment k • operator (E a k) by
167           simp only [smul_add,Finset.sum_add_distrib],add_apply,map_add,hF a z,hE a z,add_zero]
168 
169 open MeasureTheory in
170 /-- A complete box-certified polynomial family is an actual probability
171 instrument once its separate exact mass constraints hold. -/
172 noncomputable def boxInstrument {A : Type*} {n : ℕ}
173     (F : A → Fin n → State →L[ℝ] State) (E : A → Fin n → Coefficient)
174     (r : Fin n → ℝ) (kappa : A → ℝ → ℝ)
175     (hE : ∀ a k i j,|E a k i j|≤r k)
176     (hmargin : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → kappa a u≤sigma (PolynomialGram.operatorPolynomial (F a) u))
177     (hcover : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → 9*(∑ k,r k)≤kappa a u)
178     (hF : ∀ a z,probabilityCone.mass ((∫ u,PolynomialGram.operatorPolynomial (F a) u
179       ∂UniformIntervalMoments.measure) z)=probabilityCone.mass z)
180     (hzero : ∀ a z,probabilityCone.mass ((∫ u,PolynomialGram.operatorPolynomial (fun k => operator (E a k)) u
181       ∂UniformIntervalMoments.measure) z)=0) :
182     ContinuousInstrument.DensityInstrument (A := A) (probabilityCone (V := Spatial)) UniformIntervalMoments.measure :=
183   uncertainInstrument F (fun a k => operator (E a k)) kappa
184     (fun _ _ => 3*∑ k,r k) (fun _ _ => 6*∑ k,r k)
185     (boxCertificate F E r kappa hE hmargin hcover) (exact_mass_with_error F E hF hzero)
186 
187 open MeasureTheory in
188 theorem box_record_probability {A : Type*} [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
189     {n : ℕ} (F : A → Fin n → State →L[ℝ] State) (E : A → Fin n → Coefficient)
190     (r : Fin n → ℝ) (kappa : A → ℝ → ℝ)
191     (hE : ∀ a k i j,|E a k i j|≤r k)
192     (hmargin : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → kappa a u≤sigma (PolynomialGram.operatorPolynomial (F a) u))
193     (hcover : ∀ a u,u∈Set.Icc (-1 : ℝ) 1 → 9*(∑ k,r k)≤kappa a u)
194     (hF : ∀ a z,probabilityCone.mass ((∫ u,PolynomialGram.operatorPolynomial (F a) u
195       ∂UniformIntervalMoments.measure) z)=probabilityCone.mass z)
196     (hzero : ∀ a z,probabilityCone.mass ((∫ u,PolynomialGram.operatorPolynomial (fun k => operator (E a k)) u
197       ∂UniformIntervalMoments.measure) z)=0)
198     (π : ContinuousRecords.Policy (A := A) (Y := ℝ))
199     (z : ContinuousInstrument.DensityInstrument.State (probabilityCone (V := Spatial))) (N : ℕ) :
200     IsProbabilityMeasure (ContinuousRecords.recordLaw (boxInstrument F E r kappa hE hmargin hcover hF hzero) π z.1 N) :=
201   ContinuousRecords.recordLaw_probability _ π z N
202 
203 end Komorebi.LSM.CoefficientBox3

Back to source controls