PolynomialGram.lean

1 import KomorebiLSM.UniformIntervalMoments
2 import KomorebiLSM.ContinuousInstrument
3 import KomorebiLSM.FiniteInstrument
4 import Mathlib.Analysis.Matrix.PosDef
5 
6 /-! P53: polynomial interval Gram matrices and their literal Choi contraction.
7 The pair `(i,p)` denotes output row `i` and input column `p`. Positivity is
8 derived from a positive-semidefinite Choi matrix, rather than assumed of its
9 contraction map. -/
10 set_option autoImplicit false
11 namespace Komorebi.LSM.PolynomialGram
12 open Matrix MeasureTheory
13 open scoped BigOperators
14 
15 variable {D N : Type*} [Fintype D] [Fintype N]
16 
17 /-- The literal output/input-index Choi contraction. -/
18 noncomputable def choiAction (F : Matrix (D × D) (D × D) ℝ) :
19     Matrix D D ℝ →ₗ[ℝ] Matrix D D ℝ where
20   toFun X i j := ∑ p, ∑ q, F (i,p) (j,q) * X p q
21   map_add' X Y := by
22     ext i j
23     change (∑ p, ∑ q, F (i,p) (j,q) * (X p q + Y p q)) = _ + _
24     simp only [mul_add, Finset.sum_add_distrib]
25   map_smul' a X := by
26     ext i j
27     change (∑ p, ∑ q, F (i,p) (j,q) * (a * X p q)) = a * (∑ p, ∑ q, F (i,p) (j,q) * X p q)
28     simp only [Finset.mul_sum]
29     apply Finset.sum_congr rfl
30     intro p _
31     apply Finset.sum_congr rfl
32     intro q _
33     ring
34 
35 @[simp] theorem choiAction_apply (F : Matrix (D × D) (D × D) ℝ)
36     (X : Matrix D D ℝ) (i j : D) :
37     choiAction F X i j = ∑ p, ∑ q, F (i,p) (j,q) * X p q := rfl
38 
39 /-- A weighted vectorized rank-one matrix contracts to its actual congruence. -/
40 theorem choi_rank_one (K : Matrix D D ℝ) (w : ℝ) (X : Matrix D D ℝ) :
41     choiAction (fun s t => w * K s.1 s.2 * K t.1 t.2) X =
42       w • (K * X * K.transpose) := by
43   ext i j
44   change (∑ p, ∑ q, (w * K i p * K j q) * X p q) = _
45   rw [Matrix.smul_apply, AveragedCongruence.congruence_entry]
46   simp only [smul_eq_mul, Finset.mul_sum]
47   apply Finset.sum_congr rfl
48   intro p _
49   apply Finset.sum_congr rfl
50   intro q _
51   ring
52 
53 /-- Spectral decomposition supplies nonnegative real congruence factors from
54 the actual positive-semidefinite matrix. Factors need not be polynomial. -/
55 theorem choi_factorization [DecidableEq D] {F : Matrix (D × D) (D × D) ℝ} (hF : F.PosSemidef) :
56     ∃ (w : D × D → ℝ) (K : D × D → Matrix D D ℝ),
57       (∀ k, 0 ≤ w k) ∧
58       (∀ s t, F s t = ∑ k, w k * K k s.1 s.2 * K k t.1 t.2) ∧
59       (∀ X, choiAction F X = ∑ k, w k • (K k * X * (K k).transpose)) := by
60   let U : Matrix (D × D) (D × D) ℝ := hF.isHermitian.eigenvectorUnitary
61   let w := hF.isHermitian.eigenvalues
62   let K : D × D → Matrix D D ℝ := fun k i p => U (i,p) k
63   have hentry (s t : D × D) : F s t = ∑ k, w k * K k s.1 s.2 * K k t.1 t.2 := by
64     have hdiag : F = U * diagonal w * U.transpose := by
65       simpa only [Unitary.conjStarAlgAut_apply, Matrix.star_eq_conjTranspose,
66         Matrix.conjTranspose_eq_transpose_of_trivial, RCLike.ofReal_real_eq_id,
67         Function.id_comp] using hF.isHermitian.spectral_theorem
68     rw [hdiag, Matrix.mul_apply]
69     simp only [Matrix.mul_diagonal, Matrix.transpose_apply]
70     apply Finset.sum_congr rfl
71     intro k _
72     dsimp [K]
73     ring
74   refine ⟨w,K,hF.eigenvalues_nonneg,hentry,?_⟩
75   intro X
76   ext i j
77   simp only [choiAction_apply, hentry, Finset.sum_mul, Matrix.sum_apply,
78     Matrix.smul_apply, smul_eq_mul, AveragedCongruence.congruence_entry,
79     Finset.mul_sum]
80   calc
81     _ = ∑ p, ∑ k, ∑ q, w k * K k i p * K k j q * X p q := by
82       apply Finset.sum_congr rfl
83       intro p _
84       exact Finset.sum_comm
85     _ = ∑ k, ∑ p, ∑ q, w k * K k i p * K k j q * X p q := Finset.sum_comm
86     _ = _ := by
87       apply Finset.sum_congr rfl
88       intro k _
89       apply Finset.sum_congr rfl
90       intro p _
91       apply Finset.sum_congr rfl
92       intro q _
93       ring
94 
95 /-- Choi positivity entails positivity of the contracted map. -/
96 theorem choi_positive [DecidableEq D] {F : Matrix (D × D) (D × D) ℝ} (hF : F.PosSemidef)
97     {X : Matrix D D ℝ} (hX : X.PosSemidef) : (choiAction F X).PosSemidef := by
98   obtain ⟨w,K,hw,_,he⟩ := choi_factorization hF
99   rw [he X]
100   apply Matrix.posSemidef_sum
101   intro k _
102   apply Matrix.PosSemidef.smul _ (hw k)
103   simpa only [Matrix.conjTranspose_eq_transpose_of_trivial] using
104     hX.mul_mul_conjTranspose_same (K k)
105 
106 variable [DecidableEq N]
107 
108 /-- `q+1` blocks of powers of `u`, each multiplying the identity. -/
109 
110 noncomputable def powerStack (q : ℕ) (u : ℝ) :
111     Matrix (Fin (q+1) × N) N ℝ := fun ki j => u ^ (ki.1 : ℕ) * if ki.2=j then 1 else 0
112 
113 /-- A polynomial Gram square is positive at every real argument. -/
114 theorem gram_square_positive (q : ℕ) (G : Matrix (Fin (q+1) × N) (Fin (q+1) × N) ℝ)
115     (hG : G.PosSemidef) (u : ℝ) :
116     ((powerStack q u).transpose * G * powerStack q u).PosSemidef := by
117   simpa only [Matrix.conjTranspose_eq_transpose_of_trivial] using
118     hG.conjTranspose_mul_mul_same (powerStack q u)
119 
120 /-- At `q=0` the second term is omitted, rather than creating an artificial
121 degree-minus-one block. -/
122 noncomputable def intervalGram : (q : ℕ) →
123     Matrix (Fin (q+1) × N) (Fin (q+1) × N) ℝ →
124     Matrix (Fin q × N) (Fin q × N) ℝ → ℝ → Matrix N N ℝ
125   | 0, G₀, _, u => (powerStack 0 u).transpose * G₀ * powerStack 0 u
126   | k+1, G₀, G₁, u => (powerStack (k+1) u).transpose * G₀ * powerStack (k+1) u +
127       (1-u^2) • ((powerStack k u).transpose * G₁ * powerStack k u)
128 
129 theorem interval_gram_positive (q : ℕ)
130     (G₀ : Matrix (Fin (q+1) × N) (Fin (q+1) × N) ℝ)
131     (G₁ : Matrix (Fin q × N) (Fin q × N) ℝ)
132     (hG₀ : G₀.PosSemidef) (hG₁ : G₁.PosSemidef)
133     (u : ℝ) (hu : u ∈ Set.Icc (-1 : ℝ) 1) : (intervalGram q G₀ G₁ u).PosSemidef := by
134   cases q with
135   | zero => simpa only [intervalGram] using gram_square_positive 0 G₀ hG₀ u
136   | succ q =>
137     apply Matrix.PosSemidef.add (gram_square_positive (q+1) G₀ hG₀ u)
138     apply Matrix.PosSemidef.smul (gram_square_positive q G₁ hG₁ u)
139     nlinarith [hu.1,hu.2]
140 
141 theorem interval_gram_zero (G₀ : Matrix (Fin 1 × N) (Fin 1 × N) ℝ)
142     (G₁ : Matrix (Fin 0 × N) (Fin 0 × N) ℝ) (u : ℝ) :
143     intervalGram 0 G₀ G₁ u = fun i j => G₀ (0,i) (0,j) := by
144   ext i j
145   simp [intervalGram,powerStack,Matrix.mul_apply,Fintype.sum_prod_type]
146 
147 section PolynomialIdentities
148 open Polynomial
149 variable {M L : Type*}
150 
151 /-- Entrywise evaluation of a finite matrix polynomial. -/
152 noncomputable def evalMatrix (P : Matrix M N ℝ[X]) (u : ℝ) : Matrix M N ℝ :=
153   fun i j => (P i j).eval u
154 
155 omit [Fintype N] [DecidableEq N] in
156 theorem evalMatrix_add (P Q : Matrix M N ℝ[X]) (u : ℝ) :
157     evalMatrix (P+Q) u = evalMatrix P u + evalMatrix Q u := by
158   ext i j
159   exact Polynomial.eval_add
160 
161 omit [DecidableEq N] in
162 theorem evalMatrix_mul (P : Matrix M N ℝ[X]) (Q : Matrix N L ℝ[X]) (u : ℝ) :
163     evalMatrix (P*Q) u = evalMatrix P u * evalMatrix Q u := by
164   ext i j
165   simp [evalMatrix,Matrix.mul_apply,Polynomial.eval_finsetSum]
166 
167 omit [Fintype N] [DecidableEq N] in
168 /-- Formal identity of bounded-degree matrix polynomials is exactly a finite
169 list of coefficient equalities. It is equivalent to equality at every real point. -/
170 theorem polynomial_identity_finite (P Q : Matrix M N ℝ[X]) (bound : ℕ)
171     (hP : ∀ i j,(P i j).natDegree ≤ bound) (hQ : ∀ i j,(Q i j).natDegree ≤ bound) :
172     (∀ u, evalMatrix P u = evalMatrix Q u) ↔
173       (∀ i j (k : Fin (bound+1)),(P i j).coeff k = (Q i j).coeff k) := by
174   constructor
175   · intro he i j k
176     have hpq : P i j=Q i j := Polynomial.funext (fun u => congrFun (congrFun (he u) i) j)
177     rw [hpq]
178   · intro hc u
179     have hpq : P=Q := by
180       ext i j k
181       by_cases hk : k < bound+1
182       · exact hc i j ⟨k,hk⟩
183       · rw [Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt (hP i j) (by omega)),
184           Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_le_of_lt (hQ i j) (by omega))]
185     rw [hpq]
186 
187 omit [Fintype N] [DecidableEq N] in
188 /-- Equality on the entire interval already forces equality of the finite
189 coefficient data; no sample grid is substituted for the interval. -/
190 theorem polynomial_interval_identity_finite (P Q : Matrix M N ℝ[X]) (bound : ℕ)
191     (hP : ∀ i j,(P i j).natDegree≤bound) (hQ : ∀ i j,(Q i j).natDegree≤bound) :
192     (∀ u∈Set.Icc (-1 : ℝ) 1,evalMatrix P u=evalMatrix Q u) ↔
193       (∀ i j (k : Fin (bound+1)),(P i j).coeff k=(Q i j).coeff k) := by
194   constructor
195   · intro h
196     apply (polynomial_identity_finite P Q bound hP hQ).mp
197     intro u
198     have hpq : P=Q := by
199       funext i j
200       apply Polynomial.eq_of_infinite_eval_eq
201       apply (Set.Icc_infinite (by norm_num : (-1 : ℝ)<1)).mono
202       intro v hv
203       exact congrFun (congrFun (h v hv) i) j
204     rw [hpq]
205   · intro h u _
206     exact (polynomial_identity_finite P Q bound hP hQ).mpr h u
207 
208 /-- Polynomial version of the stacked monomials. -/
209 noncomputable def powerStackPolynomial (q : ℕ) :
210     Matrix (Fin (q+1) × N) N ℝ[X] := fun ki j =>
211       Polynomial.X ^ (ki.1 : ℕ) * if ki.2=j then 1 else 0
212 
213 noncomputable def constantMatrix (G : Matrix M N ℝ) : Matrix M N ℝ[X] :=
214   fun i j => Polynomial.C (G i j)
215 
216 /-- This is an actual matrix polynomial, including its explicit zero-degree case. -/
217 noncomputable def intervalGramPolynomial : (q : ℕ) →
218     Matrix (Fin (q+1) × N) (Fin (q+1) × N) ℝ →
219     Matrix (Fin q × N) (Fin q × N) ℝ → Matrix N N ℝ[X]
220   | 0,G₀,_ => (powerStackPolynomial 0).transpose * constantMatrix G₀ * powerStackPolynomial 0
221   | k+1,G₀,G₁ => (powerStackPolynomial (k+1)).transpose * constantMatrix G₀ * powerStackPolynomial (k+1) +
222       ((1 : ℝ[X])-Polynomial.X^2) • ((powerStackPolynomial k).transpose * constantMatrix G₁ * powerStackPolynomial k)
223 
224 omit [Fintype N] [DecidableEq N] in
225 theorem evalMatrix_transpose (P : Matrix M N ℝ[X]) (u : ℝ) :
226     evalMatrix P.transpose u = (evalMatrix P u).transpose := rfl
227 
228 omit [Fintype N] [DecidableEq N] in
229 theorem evalMatrix_scalar (p : ℝ[X]) (P : Matrix M N ℝ[X]) (u : ℝ) :
230     evalMatrix (p • P) u = p.eval u • evalMatrix P u := by
231   ext i j
232   exact Polynomial.eval_mul
233 
234 omit [Fintype N] [DecidableEq N] in
235 theorem evalMatrix_constant (G : Matrix M N ℝ) (u : ℝ) :
236     evalMatrix (constantMatrix G) u=G := by
237   ext i j
238   exact Polynomial.eval_C
239 
240 omit [Fintype N] in
241 theorem powerStackPolynomial_eval (q : ℕ) (u : ℝ) :
242     evalMatrix (powerStackPolynomial (N := N) q) u=powerStack q u := by
243   ext ki j
244   by_cases h : ki.2=j <;> simp [evalMatrix,powerStackPolynomial,powerStack,h]
245 
246 theorem intervalGramPolynomial_eval (q : ℕ)
247     (G₀ : Matrix (Fin (q+1) × N) (Fin (q+1) × N) ℝ)
248     (G₁ : Matrix (Fin q × N) (Fin q × N) ℝ) (u : ℝ) :
249     evalMatrix (intervalGramPolynomial q G₀ G₁) u = intervalGram q G₀ G₁ u := by
250   cases q <;>
251     simp only [intervalGramPolynomial,intervalGram,evalMatrix_add,evalMatrix_scalar,
252       evalMatrix_mul,evalMatrix_transpose,evalMatrix_constant,powerStackPolynomial_eval,
253       Polynomial.eval_sub,Polynomial.eval_one,Polynomial.eval_pow,Polynomial.eval_X]
254 
255 /-- Polynomial Choi contraction uses the same explicit output/input pairs. -/
256 noncomputable def choiPolynomial (F : Matrix (D × D) (D × D) ℝ[X])
257     (X : Matrix D D ℝ) : Matrix D D ℝ[X] :=
258   fun i j => ∑ p, ∑ q, F (i,p) (j,q) * Polynomial.C (X p q)
259 
260 theorem choiPolynomial_eval (F : Matrix (D × D) (D × D) ℝ[X])
261     (X : Matrix D D ℝ) (u : ℝ) :
262     evalMatrix (choiPolynomial F X) u=choiAction (evalMatrix F u) X := by
263   ext i j
264   change (∑ p, ∑ q, F (i,p) (j,q) * Polynomial.C (X p q)).eval u =
265     ∑ p, ∑ q, (F (i,p) (j,q)).eval u * X p q
266   simp [Polynomial.eval_finsetSum]
267 
268 end PolynomialIdentities
269 
270 section PolynomialOperators
271 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
272 
273 /-- A declared finite power expansion in continuous linear operators. -/
274 noncomputable def operatorPolynomial {n : ℕ} (B : Fin n → E →L[ℝ] E) (u : ℝ) : E →L[ℝ] E :=
275   ∑ k : Fin n, u ^ (k : ℕ) • B k
276 
277 /-- The Bochner integral is defined for the whole operator, not just its entries. -/
278 theorem continuous_uniform_integrable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
279     {f : ℝ → F} (hf : Continuous f) : Integrable f UniformIntervalMoments.measure := by
280   unfold UniformIntervalMoments.measure AveragedCongruence.uniformInterval ProbabilityTheory.cond
281   exact (hf.intervalIntegrable (-1) 1).1.smul_measure (by simp)
282 
283 theorem operatorPolynomial_continuous {n : ℕ} (B : Fin n → E →L[ℝ] E) :
284     Continuous (operatorPolynomial B) := by
285   unfold operatorPolynomial
286   fun_prop
287 
288 theorem operatorPolynomial_integrable {n : ℕ} (B : Fin n → E →L[ℝ] E) :
289     Integrable (operatorPolynomial B) UniformIntervalMoments.measure :=
290   continuous_uniform_integrable (operatorPolynomial_continuous B)
291 
292 /-- Exact normalization of a polynomial uses only finitely many actual moments. -/
293 theorem operatorPolynomial_integral [CompleteSpace E] {n : ℕ} (B : Fin n → E →L[ℝ] E) :
294     (∫ u,operatorPolynomial B u∂UniformIntervalMoments.measure) =
295       ∑ k : Fin n, UniformIntervalMoments.moment k • B k := by
296   unfold operatorPolynomial
297   rw [integral_finsetSum _ (fun k _ => continuous_uniform_integrable (by fun_prop))]
298   apply Finset.sum_congr rfl
299   intro k _
300   exact integral_smul_const _ _
301 
302 /-- Embed the actual finite operator coefficients, on a specified input. -/
303 noncomputable def embeddedPolynomial {n : ℕ} (J : E →ₗ[ℝ] Matrix D D ℝ)
304     (B : Fin n → E →L[ℝ] E) (z : E) : Matrix D D (Polynomial ℝ) :=
305   fun i j => Polynomial.ofFn n (fun k => J (B k z) i j)
306 
307 omit [Fintype D] in
308 theorem embeddedPolynomial_eval {n : ℕ} (J : E →ₗ[ℝ] Matrix D D ℝ)
309     (B : Fin n → E →L[ℝ] E) (z : E) (u : ℝ) :
310     evalMatrix (embeddedPolynomial J B z) u=J (operatorPolynomial B u z) := by
311   ext i j
312   simp [evalMatrix,embeddedPolynomial,UniformIntervalMoments.eval_ofFn,
313     operatorPolynomial,map_sum,Matrix.sum_apply,Matrix.smul_apply,mul_comm]
314 
315 /-- Once degrees are bounded, the entire intertwining identity is equivalent
316 to a finite coefficient test on a basis of the actual state space. -/
317 theorem polynomial_intertwining_finite {R : Type*} (b : Module.Basis R ℝ E) {n : ℕ}
318     (J : E →ₗ[ℝ] Matrix D D ℝ) (B : Fin n → E →L[ℝ] E)
319     (F : Matrix (D × D) (D × D) (Polynomial ℝ)) (bound : ℕ)
320     (hL : ∀ r i j,(embeddedPolynomial J B (b r) i j).natDegree≤bound)
321     (hR : ∀ r i j,(choiPolynomial F (J (b r)) i j).natDegree≤bound) :
322     (∀ u z,J (operatorPolynomial B u z)=choiAction (evalMatrix F u) (J z)) ↔
323       (∀ r i j (k : Fin (bound+1)),
324         (embeddedPolynomial J B (b r) i j).coeff k =
325           (choiPolynomial F (J (b r)) i j).coeff k) := by
326   constructor
327   · intro h r
328     apply (polynomial_identity_finite _ _ bound (hL r) (hR r)).mp
329     intro u
330     rw [embeddedPolynomial_eval,choiPolynomial_eval]
331     exact h u (b r)
332   · intro h u z
333     have he : J.comp (operatorPolynomial B u).toLinearMap =
334         (choiAction (evalMatrix F u)).comp J := by
335       apply b.ext
336       intro r
337       have hv := (polynomial_identity_finite _ _ bound (hL r) (hR r)).mpr (h r) u
338       rw [embeddedPolynomial_eval,choiPolynomial_eval] at hv
339       exact hv
340     exact congrArg (fun L : E →ₗ[ℝ] Matrix D D ℝ => L z) he
341 
342 /-- The Gram identity makes the actual state operator positive on the embedded
343 matrix cone at every observation point of the interval. -/
344 theorem gram_operator_positive [DecidableEq D] (J : E →ₗ[ℝ] Matrix D D ℝ)
345     {n q : ℕ} (B : Fin n → E →L[ℝ] E)
346     (G₀ : Matrix (Fin (q+1) × (D × D)) (Fin (q+1) × (D × D)) ℝ)
347     (G₁ : Matrix (Fin q × (D × D)) (Fin q × (D × D)) ℝ)
348     (hG₀ : G₀.PosSemidef) (hG₁ : G₁.PosSemidef)
349     (he : ∀ u z,J (operatorPolynomial B u z)=choiAction (intervalGram q G₀ G₁ u) (J z))
350     (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1) (z : E) (hz : (J z).PosSemidef) :
351     (J (operatorPolynomial B u z)).PosSemidef := by
352   rw [he]
353   exact choi_positive (interval_gram_positive q G₀ G₁ hG₀ hG₁ u hu) hz
354 
355 /-- The actual reference measure is supported on the declared interval. -/
356 theorem uniform_ae_interval :
357     ∀ᵐ u∂UniformIntervalMoments.measure,u∈Set.Icc (-1 : ℝ) 1 := by
358   unfold UniformIntervalMoments.measure AveragedCongruence.uniformInterval ProbabilityTheory.cond
359   apply Measure.ae_smul_measure
360   filter_upwards [ae_restrict_mem (μ := volume) measurableSet_Ioc] with u hu
361   exact ⟨hu.1.le,hu.2⟩
362 
363 /-- The exact integrated mass law is a finite collection of checks on a basis. -/
364 theorem moment_mass_finite {R : Type*} (b : Module.Basis R ℝ E) {n : ℕ}
365     (l : E →ₗ[ℝ] ℝ) (B : Fin n → E →L[ℝ] E) :
366     (∀ z,l ((∑ k : Fin n,UniformIntervalMoments.moment k • B k) z)=l z) ↔
367       (∀ r,l ((∑ k : Fin n,UniformIntervalMoments.moment k • B k) (b r))=l (b r)) := by
368   constructor
369   · intro h r
370     exact h (b r)
371   · intro h z
372     have he : l.comp (∑ k : Fin n,UniformIntervalMoments.moment k • B k).toLinearMap=l := by
373       apply b.ext
374       exact h
375     exact congrArg (fun L : E →ₗ[ℝ] ℝ => L z) he
376 
377 variable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
378 
379 /-- Polynomial Gram data construct the literal P52 density instrument. The
380 input is finite Gram positivity, polynomial identities and exact finite-moment
381 normalization, rather than an assumed positive stochastic kernel. -/
382 noncomputable def polynomialDensityInstrument [DecidableEq D]
383     {A R : Type*} [Fintype R] (b : Module.Basis R ℝ E)
384     (C : BaseNorm.ProbabilityCone E) (J : E →ₗ[ℝ] Matrix D D ℝ)
385     (hC : ∀ z,z∈C.carrier ↔ (J z).PosSemidef) {n q : ℕ}
386     (B : A → Fin n → E →L[ℝ] E)
387     (G₀ : A → Matrix (Fin (q+1) × (D × D)) (Fin (q+1) × (D × D)) ℝ)
388     (G₁ : A → Matrix (Fin q × (D × D)) (Fin q × (D × D)) ℝ)
389     (hG₀ : ∀ a,(G₀ a).PosSemidef) (hG₁ : ∀ a,(G₁ a).PosSemidef)
390     (he : ∀ a u z,J (operatorPolynomial (B a) u z)=
391       choiAction (intervalGram q (G₀ a) (G₁ a) u) (J z))
392     (hm : ∀ a r,C.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • B a k) (b r))=C.mass (b r)) :
393     ContinuousInstrument.DensityInstrument (A := A) C UniformIntervalMoments.measure where
394   op a := operatorPolynomial (B a)
395   measurable_op a := (operatorPolynomial_continuous (B a)).measurable
396   integrable_op a := operatorPolynomial_integrable (B a)
397   positive a := by
398     filter_upwards [uniform_ae_interval] with u hu
399     intro z hz
400     exact (hC _).mpr (gram_operator_positive J (B a) (G₀ a) (G₁ a) (hG₀ a) (hG₁ a)
401       (he a) u hu z ((hC z).mp hz))
402   mass_preserving a z := by
403     rw [operatorPolynomial_integral]
404     exact (moment_mass_finite b C.mass (B a)).mpr (hm a) z
405 
406 /-- A finite replayable P53 certificate. All intertwining checks are literal
407 coefficients on a finite state basis, and normalization uses actual uniform
408 moments. No operator-positivity or probability-law conclusion is a field. -/
409 structure CoefficientCertificate [DecidableEq D] {A R : Type*} [Fintype A] [Fintype R]
410     (b : Module.Basis R ℝ E) (C : BaseNorm.ProbabilityCone E)
411     (J : E →ₗ[ℝ] Matrix D D ℝ) {n : ℕ} (B : A → Fin n → E →L[ℝ] E)
412     (q bound : ℕ) where
413   gram0 : A → Matrix (Fin (q+1) × (D × D)) (Fin (q+1) × (D × D)) ℝ
414   gram1 : A → Matrix (Fin q × (D × D)) (Fin q × (D × D)) ℝ
415   gram0_positive : ∀ a,(gram0 a).PosSemidef
416   gram1_positive : ∀ a,(gram1 a).PosSemidef
417   left_degree : ∀ a r i j,(embeddedPolynomial J (B a) (b r) i j).natDegree≤bound
418   right_degree : ∀ a r i j,
419     (choiPolynomial (intervalGramPolynomial q (gram0 a) (gram1 a)) (J (b r)) i j).natDegree≤bound
420   coefficients : ∀ a r i j (k : Fin (bound+1)),
421     (embeddedPolynomial J (B a) (b r) i j).coeff k =
422       (choiPolynomial (intervalGramPolynomial q (gram0 a) (gram1 a)) (J (b r)) i j).coeff k
423   mass : ∀ a r,C.mass ((∑ k : Fin n,UniformIntervalMoments.moment k • B a k) (b r))=C.mass (b r)
424 
425 namespace CoefficientCertificate
426 variable [DecidableEq D] {A R : Type*} [Fintype A] [Fintype R]
427 variable {b : Module.Basis R ℝ E} {C : BaseNorm.ProbabilityCone E}
428 variable {J : E →ₗ[ℝ] Matrix D D ℝ} {n q bound : ℕ} {B : A → Fin n → E →L[ℝ] E}
429 variable (W : CoefficientCertificate b C J B q bound)
430 
431 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
432 /-- The finite coefficient data imply the full identity on every input and
433 every real observation, hence on the entire interval. -/
434 theorem intertwines (a : A) (u : ℝ) (z : E) :
435     J (operatorPolynomial (B a) u z)=choiAction (intervalGram q (W.gram0 a) (W.gram1 a) u) (J z) := by
436   have he := (polynomial_intertwining_finite b J (B a)
437     (intervalGramPolynomial q (W.gram0 a) (W.gram1 a)) bound
438     (W.left_degree a) (W.right_degree a)).mpr (W.coefficients a) u z
439   rwa [intervalGramPolynomial_eval] at he
440 
441 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
442 include W in
443 /-- Whole-interval positivity is derived from the finite witness. -/
444 theorem positive (a : A) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1)
445     (z : E) (hz : (J z).PosSemidef) : (J (operatorPolynomial (B a) u z)).PosSemidef :=
446   gram_operator_positive J (B a) (W.gram0 a) (W.gram1 a)
447     (W.gram0_positive a) (W.gram1_positive a) (W.intertwines a) u hu z hz
448 
449 /-- The checked finite data build P52's continuous probability instrument. -/
450 noncomputable def instrument
451     (hC : ∀ z,z∈C.carrier ↔ (J z).PosSemidef) :
452     ContinuousInstrument.DensityInstrument (A := A) C UniformIntervalMoments.measure :=
453   polynomialDensityInstrument b C J hC B W.gram0 W.gram1
454     W.gram0_positive W.gram1_positive W.intertwines W.mass
455 
456 omit [MeasurableSpace E] [BorelSpace E] in
457 @[simp] theorem instrument_op (hC : ∀ z,z∈C.carrier ↔ (J z).PosSemidef) (a : A) (u : ℝ) :
458     (W.instrument hC).op a u=operatorPolynomial (B a) u := rfl
459 
460 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
461 include W in
462 /-- Every finite chronological product stays in the actual embedded PSD cone
463 at every interval-valued record, not merely almost everywhere or on a grid. -/
464 theorem word_positive (word : List (A × ℝ))
465     (hword : ∀ s∈word,s.2∈Set.Icc (-1 : ℝ) 1) (z : E) (hz : (J z).PosSemidef) :
466     (J (FiniteInstruments.wordAction
467       (fun s : A × ℝ => (operatorPolynomial (B s.1) s.2).toLinearMap) word z)).PosSemidef := by
468   induction word generalizing z with
469   | nil => simpa only [FiniteInstruments.wordAction_nil,LinearMap.id_apply] using hz
470   | cons s word ih =>
471     rw [FiniteInstruments.wordAction_cons,LinearMap.comp_apply]
472     apply ih
473     · intro t ht
474       exact hword t (List.mem_cons_of_mem s ht)
475     · exact W.positive s.1 s.2 (hword s (List.mem_cons_self)) z hz
476 
477 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
478 include W in
479 /-- The product mass is a nonnegative density at each interval-valued record;
480 density values are not incorrectly bounded by one. -/
481 theorem word_mass_nonnegative (hC : ∀ z,z∈C.carrier ↔ (J z).PosSemidef)
482     (word : List (A × ℝ)) (hword : ∀ s∈word,s.2∈Set.Icc (-1 : ℝ) 1)
483     (z : E) (hz : z∈C.carrier) :
484     0≤C.mass (FiniteInstruments.wordAction
485       (fun s : A × ℝ => (operatorPolynomial (B s.1) s.2).toLinearMap) word z) :=
486   C.mass_nonneg ((hC _).mpr (W.word_positive word hword z ((hC z).mp hz)))
487 
488 omit [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] in
489 include W in
490 /-- The exact normalized update belongs to the same certified base at every
491 interval point with positive density. -/
492 theorem normalized_update (hC : ∀ z,z∈C.carrier ↔ (J z).PosSemidef)
493     (a : A) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1)
494     (z : E) (hz : z∈C.base) (hp : 0<C.mass (operatorPolynomial (B a) u z)) :
495     (C.mass (operatorPolynomial (B a) u z))⁻¹ • operatorPolynomial (B a) u z∈C.base := by
496   refine ⟨C.smul_mem (inv_nonneg.mpr hp.le)
497     ((hC _).mpr (W.positive a u hu z ((hC z).mp hz.1))),?_⟩
498   rw [map_smul,smul_eq_mul]
499   exact inv_mul_cancel₀ hp.ne'
500 
501 end CoefficientCertificate
502 
503 end PolynomialOperators
504 
505 end Komorebi.LSM.PolynomialGram

Back to source controls