PredictiveCompletion.lean

1 import KomorebiLSM.InvariantCompletion
2 import Mathlib.LinearAlgebra.Dual.Lemmas
3 
4 /-! P8: apply the finite invariant-space construction to observable rows.
5 The observation map and reduced transitions are constructed, then connected
6 to arbitrary finite bases and to the row spaces of competing summaries. -/
7 set_option autoImplicit false
8 open scoped BigOperators
9 namespace Komorebi.LSM
10 open Module
11 universe u v w
12 variable {K : Type u} [Field K]
13 variable {X : Type v} [AddCommGroup X] [Module K X]
14 variable {I : Type w}
15 
16 /-- Evaluation of all observables in a declared row space. -/
17 def observableState (W : Submodule K (Dual K X)) : X →ₗ[K] Dual K W :=
18   W.subtype.dualMap.comp (Dual.eval K X)
19 
20 @[simp] theorem observableState_apply (W : Submodule K (Dual K X)) (x : X) (w : W) :
21     observableState W x w = (w : Dual K X) x := rfl
22 
23 /-- The row pullback restricted to an invariant observable space. -/
24 def restrictedPullback (L : I → X →ₗ[K] X) (W : Submodule K (Dual K X))
25     (hW : CommonInvariant (fun i => (L i).dualMap) W) (i : I) : W →ₗ[K] W :=
26   (L i).dualMap.restrict (fun w hw => hW i (Submodule.mem_map.mpr ⟨w, hw, rfl⟩))
27 
28 /-- The dual of the row pullback evolves the evaluated state. -/
29 def observableTransition (L : I → X →ₗ[K] X) (W : Submodule K (Dual K X))
30     (hW : CommonInvariant (fun i => (L i).dualMap) W) (i : I) :
31     Dual K W →ₗ[K] Dual K W := (restrictedPullback L W hW i).dualMap
32 
33 /-- Exact current-state closure follows from row invariance. -/
34 theorem observableState_closed (L : I → X →ₗ[K] X) (W : Submodule K (Dual K X))
35     (hW : CommonInvariant (fun i => (L i).dualMap) W) (i : I) :
36     (observableTransition L W hW i).comp (observableState W) =
37       (observableState W).comp (L i) := by
38   ext x w
39   rfl
40 
41 /-- Restricting the completed state recovers the initial observable state. -/
42 theorem observableState_retains (W₀ W : Submodule K (Dual K X)) (h : W₀ ≤ W) :
43     (Submodule.inclusion h).dualMap.comp (observableState W) = observableState W₀ := by
44   ext x w
45   rfl
46 
47 /-- In finite dimension this state space is exactly realizable, not padded. -/
48 theorem observableState_surjective [FiniteDimensional K X]
49     (W : Submodule K (Dual K X)) : Function.Surjective (observableState W) := by
50   intro z
51   obtain ⟨f, hf⟩ := (Subspace.dualRestrict_surjective (W := W)) z
52   refine ⟨(Module.evalEquiv K X).symm f, ?_⟩
53   ext w
54   change (w : Dual K X) ((Module.evalEquiv K X).symm f) = z w
55   rw [Module.apply_evalEquiv_symm_apply]
56   exact congrArg (fun g : Dual K W => g w) hf
57 
58 /-- The state dimension equals the completed row dimension. -/
59 theorem observableState_dimension (W : Submodule K (Dual K X)) :
60     finrank K (Dual K W) = finrank K W := by
61   simpa using (Subspace.dual_finrank_eq (K := K) (V := W))
62 
63 /-- Basis-independent completion of the initial observation rows. -/
64 noncomputable def predictiveCompletion (L : I → X →ₗ[K] X)
65     (W₀ : Submodule K (Dual K X)) : Submodule K (Dual K X) :=
66   invariantCompletion (fun i => (L i).dualMap) W₀
67 
68 theorem predictiveCompletion_isLeast [FiniteDimensional K X]
69     (L : I → X →ₗ[K] X) (W₀ : Submodule K (Dual K X)) :
70     IsLeast {W : Submodule K (Dual K X) |
71       W₀ ≤ W ∧ CommonInvariant (fun i => (L i).dualMap) W}
72       (predictiveCompletion L W₀) := invariantCompletion_isLeast _ _
73 
74 /-- The stopping bound is the original signal dimension deficit. -/
75 theorem predictiveCompletion_stopping_bound [FiniteDimensional K X]
76     (L : I → X →ₗ[K] X) (W₀ : Submodule K (Dual K X)) :
77     ∃ n ≤ finrank K X - finrank K W₀,
78       invariantSequence (fun i => (L i).dualMap) W₀ (n+1) =
79         invariantSequence (fun i => (L i).dualMap) W₀ n := by
80   simpa only [Subspace.dual_finrank_eq] using
81     invariantSequence_exists_stable (fun i => (L i).dualMap) W₀
82 
83 section Coordinates
84 variable {J : Type*} [Fintype J]
85 variable {W : Submodule K (Dual K X)}
86 
87 /-- The rows of an arbitrary basis are the matrix R in the manuscript. -/
88 noncomputable def basisObservation (b : Basis J K W) : X →ₗ[K] (J → K) :=
89   LinearMap.pi (fun j => (b j : Dual K X))
90 
91 /-- Reading out any row using its finite basis coefficients. -/
92 noncomputable def basisRowReadout (b : Basis J K W) (w : W) : (J → K) →ₗ[K] K :=
93   ∑ j, (b.repr w j) • (LinearMap.proj j : (J → K) →ₗ[K] K)
94 
95 theorem basisRowReadout_correct (b : Basis J K W) (w : W) (x : X) :
96     basisRowReadout b w (basisObservation b x) = (w : Dual K X) x := by
97   have h := congrArg (fun z : W => (z : Dual K X) x) (b.sum_repr w)
98   simp only [Submodule.coe_sum, Submodule.coe_smul, LinearMap.sum_apply,
99     LinearMap.smul_apply, smul_eq_mul] at h
100   simpa only [basisRowReadout, basisObservation, LinearMap.sum_apply,
101     LinearMap.smul_apply, LinearMap.proj_apply, LinearMap.pi_apply, smul_eq_mul] using h
102 
103 /-- A finite matrix acting on the basis-evaluation state. -/
104 noncomputable def basisTransition (L : I → X →ₗ[K] X)
105     (hW : CommonInvariant (fun i => (L i).dualMap) W)
106     (b : Basis J K W) (i : I) : (J → K) →ₗ[K] (J → K) :=
107   LinearMap.pi (fun j => basisRowReadout b (restrictedPullback L W hW i (b j)))
108 
109 /-- R L_i = B_i R, for any chosen basis of the invariant row space. -/
110 theorem basisTransition_correct (L : I → X →ₗ[K] X)
111     (hW : CommonInvariant (fun i => (L i).dualMap) W)
112     (b : Basis J K W) (i : I) :
113     (basisTransition L hW b i).comp (basisObservation b) =
114       (basisObservation b).comp (L i) := by
115   ext x j
116   exact basisRowReadout_correct b (restrictedPullback L W hW i (b j)) x
117 
118 /-- H R recovers every specified initial row, not only a fitted sample. -/
119 theorem basisReadout_correct {O : Type*} (b : Basis J K W) (rows : O → W) :
120     (LinearMap.pi (fun o => basisRowReadout b (rows o))).comp (basisObservation b) =
121       LinearMap.pi (fun o => (rows o : Dual K X)) := by
122   ext x o
123   exact basisRowReadout_correct b (rows o) x
124 
125 omit [Fintype J] in
126 /-- The matrix rows are independent because they are an actual subspace basis. -/
127 theorem basisObservation_independent (b : Basis J K W) :
128     LinearIndependent K (fun j => (LinearMap.proj j : (J → K) →ₗ[K] K).comp
129       (basisObservation b)) := by
130   change LinearIndependent K (fun j => (b j : Dual K X))
131   intro a c h
132   apply b.linearIndependent
133   apply Subtype.ext
134   simpa only [Finsupp.linearCombination_apply, Finsupp.sum,
135     Submodule.coe_sum, Submodule.coe_smul] using h
136 
137 end Coordinates
138 
139 /-- Every summary closed under the dynamics has an invariant row space. -/
140 theorem closed_summary_row_invariant
141     {Z : Type*} [AddCommGroup Z] [Module K Z]
142     (L : I → X →ₗ[K] X) (R : X →ₗ[K] Z) (B : I → Z →ₗ[K] Z)
143     (h : ∀ i, R.comp (L i) = (B i).comp R) :
144     CommonInvariant (fun i => (L i).dualMap) (LinearMap.range R.dualMap) := by
145   intro i w hw
146   obtain ⟨v, hv, rfl⟩ := Submodule.mem_map.mp hw
147   obtain ⟨f, rfl⟩ := hv
148   refine ⟨(B i).dualMap f, ?_⟩
149   ext x
150   exact congrArg f (congrArg (fun g : X →ₗ[K] Z => g x) (h i)).symm
151 
152 /-- Retaining an output by a linear readout contains its entire row space. -/
153 theorem retained_summary_row_le
154     {Y Z : Type*} [AddCommGroup Y] [Module K Y] [AddCommGroup Z] [Module K Z]
155     (C₀ : X →ₗ[K] Y) (R : X →ₗ[K] Z) (H : Z →ₗ[K] Y)
156     (h : C₀ = H.comp R) :
157     LinearMap.range C₀.dualMap ≤ LinearMap.range R.dualMap := by
158   rintro w ⟨f, rfl⟩
159   refine ⟨H.dualMap f, ?_⟩
160   ext x
161   exact congrArg f (congrArg (fun g : X →ₗ[K] Y => g x) h).symm
162 
163 /-- Minimality applies to any linear summary with exact readout and closure. -/
164 theorem predictiveCompletion_le_competing_summary [FiniteDimensional K X]
165     {Y Z : Type*} [AddCommGroup Y] [Module K Y] [AddCommGroup Z] [Module K Z]
166     (L : I → X →ₗ[K] X) (C₀ : X →ₗ[K] Y)
167     (R : X →ₗ[K] Z) (H : Z →ₗ[K] Y) (B : I → Z →ₗ[K] Z)
168     (retains : C₀ = H.comp R) (closes : ∀ i, R.comp (L i) = (B i).comp R) :
169     predictiveCompletion L (LinearMap.range C₀.dualMap) ≤ LinearMap.range R.dualMap :=
170   invariantCompletion_minimal _ _ _ (retained_summary_row_le C₀ R H retains)
171     (closed_summary_row_invariant L R B closes)
172 
173 /-- P8 coordinate realization, with full-row-rank R, exact readout H,
174 and action transitions B constructed from the completed row space. -/
175 theorem predictiveCompletion_coordinate_realization [FiniteDimensional K X]
176     {O : Type*} (L : I → X →ₗ[K] X) (rows : O → Dual K X) :
177     let W₀ := Submodule.span K (Set.range rows)
178     let W := predictiveCompletion L W₀
179     ∃ (R : X →ₗ[K] (Fin (finrank K W) → K))
180       (H : (Fin (finrank K W) → K) →ₗ[K] (O → K))
181       (B : I → (Fin (finrank K W) → K) →ₗ[K] (Fin (finrank K W) → K)),
182       LinearIndependent K (fun j => (LinearMap.proj j).comp R) ∧
183       H.comp R = LinearMap.pi rows ∧ ∀ i, (B i).comp R = R.comp (L i) := by
184   classical
185   let W₀ := Submodule.span K (Set.range rows)
186   let W := predictiveCompletion L W₀
187   let : Module.Free K W := Module.Free.of_divisionRing K W
188   let b := Module.finBasis K W
189   have hi : W₀ ≤ W := (predictiveCompletion_isLeast L W₀).1.1
190   have hc : CommonInvariant (fun i => (L i).dualMap) W :=
191     (predictiveCompletion_isLeast L W₀).1.2
192   let rw₀ : O → W := fun o => ⟨rows o, hi (Submodule.subset_span ⟨o, rfl⟩)⟩
193   refine ⟨basisObservation b, LinearMap.pi (fun o => basisRowReadout b (rw₀ o)),
194     basisTransition L hc b, basisObservation_independent b, ?_, ?_⟩
195   · exact basisReadout_correct b rw₀
196   · exact basisTransition_correct L hc b
197 
198 end Komorebi.LSM

Back to source controls