ContinuousPopulationBridge.lean

1 import KomorebiLSM.FiniteMomentIdentification
2 import KomorebiLSM.CertifiedTemplate
3 
4 /-! P61's population-to-instrument bridge. The dimension and degree are the
5 declared finite state and coefficient types. The population core is square in
6 that supplied dimension; no rank or degree discovery is inferred from it. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.ContinuousPopulationBridge
9 open Matrix
10 open scoped BigOperators
11 
12 abbrev State (r : ℕ) := Fin r → ℝ
13 abbrev Operator (r : ℕ) := Matrix (Fin r) (Fin r) ℝ
14 
15 /-- The literal finite matrix action as a continuous linear map. -/
16 noncomputable def matrixCLM {r : ℕ} : Operator r →ₗ[ℝ] (State r →L[ℝ] State r) :=
17   LinearMap.toContinuousLinearMap.toLinearMap.comp Matrix.toLin'.toLinearMap
18 
19 @[simp] theorem matrixCLM_apply {r : ℕ} (B : Operator r) (z : State r) :
20     matrixCLM B z=B *ᵥ z := rfl
21 
22 variable {r degree : ℕ} {A : Type*}
23 
24 noncomputable def originalCoefficients (C : A → Fin (degree+1) → Operator r)
25     (a : A) (k : Fin (degree+1)) : State r →L[ℝ] State r := matrixCLM (C a k)
26 
27 /-- These are the actual inverse-moment population-table coefficients. -/
28 noncomputable def fittedCoefficients (T S : Operator r)
29     (C : A → Fin (degree+1) → Operator r) (a : A) (k : Fin (degree+1)) :
30     State r →L[ℝ] State r :=
31   matrixCLM (FiniteMomentIdentification.reconstructedCoefficient
32     (FiniteMomentIdentification.populationCore T S)
33     (FiniteMomentIdentification.populationTable T S (C a)) k)
34 
35 /-- The coordinate isomorphism is derived from the true square population
36 core, rather than supplied as an identification conclusion. -/
37 noncomputable def populationEquiv (T S : Operator r)
38     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S)) :
39     State r ≃ₗ[ℝ] State r :=
40   LinearEquiv.ofBijective T.mulVecLin
41     ⟨Matrix.mulVec_injective_iff_isUnit.mpr
42         (FiniteMomentIdentification.core_factors_isUnit T S hcore).1,
43       Matrix.mulVec_surjective_iff_isUnit.mpr
44         (FiniteMomentIdentification.core_factors_isUnit T S hcore).1⟩
45 
46 @[simp] theorem populationEquiv_apply (T S : Operator r)
47     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S)) (z : State r) :
48     populationEquiv T S hcore z=T *ᵥ z := rfl
49 
50 theorem populationEquiv_symm_apply (T S : Operator r)
51     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S)) (z : State r) :
52     (populationEquiv T S hcore).symm z=T⁻¹ *ᵥ z := by
53   apply (populationEquiv T S hcore).injective
54   rw [LinearEquiv.apply_symm_apply,populationEquiv_apply,Matrix.mulVec_mulVec,
55     Matrix.mul_nonsing_inv T ((Matrix.isUnit_iff_isUnit_det T).mp
56       (FiniteMomentIdentification.core_factors_isUnit T S hcore).1),Matrix.one_mulVec]
57 
58 /-- Exact reconstruction is proved coefficient by coefficient. -/
59 theorem fitted_coefficient_identification (T S : Operator r)
60     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
61     (C : A → Fin (degree+1) → Operator r) (a : A) (k : Fin (degree+1)) :
62     fittedCoefficients T S C a k=matrixCLM (T * C a k * T⁻¹) := by
63   rw [fittedCoefficients,FiniteMomentIdentification.reconstructedCoefficient_eq T S hcore]
64 
65 /-- Integrating the declared polynomial coefficient family and evaluating the
66 continuous operator gives the same literal matrix density. -/
67 theorem polynomial_matrix_density (C : Fin (degree+1) → Operator r) (u : ℝ) :
68     PolynomialGram.operatorPolynomial (fun k => matrixCLM (C k)) u=
69       matrixCLM (FiniteMomentIdentification.density C u) := by
70   rw [FiniteMomentIdentification.density,map_sum]
71   simp only [map_smul]
72   rfl
73 
74 theorem fitted_density_identification (T S : Operator r)
75     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
76     (C : A → Fin (degree+1) → Operator r) (a : A) (u : ℝ) :
77     PolynomialGram.operatorPolynomial (fittedCoefficients T S C a) u=
78       matrixCLM (T * FiniteMomentIdentification.density (C a) u * T⁻¹) := by
79   change PolynomialGram.operatorPolynomial
80     (fun k => matrixCLM (FiniteMomentIdentification.reconstructedCoefficient
81       (FiniteMomentIdentification.populationCore T S)
82       (FiniteMomentIdentification.populationTable T S (C a)) k)) u=_
83   rw [polynomial_matrix_density,FiniteMomentIdentification.reconstructed_density_eq T S hcore]
84 
85 /-- The coefficient matching used by exact atlas transport is derived from
86 the population reconstruction formula, rather than assumed. -/
87 theorem population_coefficient_match (T S : Operator r)
88     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
89     (C : A → Fin (degree+1) → Operator r) (a : A) (k : Fin (degree+1)) (z : State r) :
90     fittedCoefficients T S C a k (populationEquiv T S hcore z)=
91       populationEquiv T S hcore (originalCoefficients C a k z) := by
92   rw [fitted_coefficient_identification T S hcore,populationEquiv_apply,matrixCLM_apply,
93     originalCoefficients,matrixCLM_apply,populationEquiv_apply]
94   rw [← Matrix.mulVec_mulVec,FiniteMomentIdentification.initial_test_coordinates T S hcore,
95     ← Matrix.mulVec_mulVec]
96 
97 /-- The inverse atlas recovers the literal original coefficient family too.
98 No inverse operator or record-law match is an assumed identification field. -/
99 theorem population_inverse_coefficient_match (T S : Operator r)
100     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
101     (C : A → Fin (degree+1) → Operator r) (a : A) (k : Fin (degree+1)) (x : State r) :
102     originalCoefficients C a k ((populationEquiv T S hcore).symm x)=
103       (populationEquiv T S hcore).symm (fittedCoefficients T S C a k x) := by
104   apply (populationEquiv T S hcore).injective
105   rw [LinearEquiv.apply_symm_apply]
106   have h := population_coefficient_match T S hcore C a k ((populationEquiv T S hcore).symm x)
107   simpa only [LinearEquiv.apply_symm_apply] using h.symm
108 
109 /-- Every finite fine-observation word has the reconstructed test coordinates,
110 not only the finitely many moments used to identify the coefficients. -/
111 theorem fitted_word_coordinates (T S : Operator r)
112     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
113     (C : A → Fin (degree+1) → Operator r) (word : List (A × ℝ)) (z : State r) :
114     FiniteInstruments.wordAction
115       (fun s : A × ℝ => (PolynomialGram.operatorPolynomial (fittedCoefficients T S C s.1) s.2).toLinearMap)
116       word (T *ᵥ z)=T *ᵥ FiniteMomentIdentification.wordState
117         (fun a => FiniteMomentIdentification.density (C a)) word z := by
118   induction word generalizing z with
119   | nil => rfl
120   | cons s word ih =>
121     rw [FiniteInstruments.wordAction_cons,LinearMap.comp_apply,
122       fitted_density_identification T S hcore]
123     change FiniteInstruments.wordAction
124       (fun t : A × ℝ => (PolynomialGram.operatorPolynomial (fittedCoefficients T S C t.1) t.2).toLinearMap)
125       word ((T * FiniteMomentIdentification.density (C s.1) s.2 * T⁻¹) *ᵥ (T *ᵥ z))=_
126     rw [← Matrix.mulVec_mulVec,FiniteMomentIdentification.initial_test_coordinates T S hcore,
127       ← Matrix.mulVec_mulVec,ih]
128     rfl
129 
130 /-- A checked mass-row coordinate identity carries all represented word
131 likelihoods. No stochastic validity or likelihood equality is an input field. -/
132 theorem fitted_word_likelihood (T S : Operator r)
133     (hcore : IsUnit (FiniteMomentIdentification.populationCore T S))
134     (C : A → Fin (degree+1) → Operator r)
135     (l lhat : State r →ₗ[ℝ] ℝ) (hmass : lhat.comp T.mulVecLin=l)
136     (word : List (A × ℝ)) (z : State r) :
137     lhat (FiniteInstruments.wordAction
138       (fun s : A × ℝ => (PolynomialGram.operatorPolynomial (fittedCoefficients T S C s.1) s.2).toLinearMap)
139       word (T *ᵥ z))=
140       l (FiniteMomentIdentification.wordState (fun a => FiniteMomentIdentification.density (C a)) word z) := by
141   rw [fitted_word_coordinates T S hcore]
142   exact congrArg (fun L : State r →ₗ[ℝ] ℝ => L
143     (FiniteMomentIdentification.wordState (fun a => FiniteMomentIdentification.density (C a)) word z)) hmass
144 
145 end Komorebi.LSM.ContinuousPopulationBridge

Back to source controls