BehaviorSpace.lean

1 import KomorebiLSM.FiniteInstrument
2 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
3 
4 /-! P27: the canonical behavior space is built from actual future-test columns.
5 A shift on the full test-function space restricts to their span. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.Behavior
8 open scoped BigOperators
9 open FiniteInstruments
10 variable {S : Type*}
11 
12 /-- Chronological history followed by a prescribed future test. -/
13 def column (f : List S → ℝ) (h : List S) : List S → ℝ := fun t => f (h ++ t)
14 
15 /-- The state space is a span of columns, not a supplied latent representation. -/
16 noncomputable def space (f : List S → ℝ) : Submodule ℝ (List S → ℝ) :=
17   Submodule.span ℝ (Set.range (column f))
18 
19 noncomputable def history (f : List S → ℝ) (h : List S) : space f :=
20   ⟨column f h, Submodule.subset_span ⟨h,rfl⟩⟩
21 
22 @[simp] theorem history_apply (f : List S → ℝ) (h t : List S) :
23     (history f h : List S → ℝ) t = f (h ++ t) := rfl
24 
25 /-- Prepending a symbol to a test appends that symbol to its history column. -/
26 def shift (s : S) : (List S → ℝ) →ₗ[ℝ] (List S → ℝ) where
27   toFun v t := v (s :: t)
28   map_add' _ _ := rfl
29   map_smul' _ _ := rfl
30 
31 @[simp] theorem shift_column (f : List S → ℝ) (s : S) (h : List S) :
32     shift s (column f h) = column f (h ++ [s]) := by
33   funext t
34   simp [shift, column, List.append_assoc]
35 
36 theorem shift_mem (f : List S → ℝ) (s : S) (v : List S → ℝ)
37     (hv : v ∈ space f) : shift s v ∈ space f := by
38   induction hv using Submodule.span_induction with
39   | mem v hv =>
40     obtain ⟨h,rfl⟩ := hv
41     rw [shift_column]
42     exact Submodule.subset_span ⟨h ++ [s],rfl⟩
43   | zero => simp
44   | add x y hx hy ihx ihy => simpa using (space f).add_mem ihx ihy
45   | smul a x hx ih => simpa using (space f).smul_mem a ih
46 
47 noncomputable def branch (f : List S → ℝ) (s : S) : space f →ₗ[ℝ] space f :=
48   (shift s).restrict (shift_mem f s)
49 
50 @[simp] theorem branch_apply (f : List S → ℝ) (s : S) (v : space f) (t : List S) :
51     (branch f s v : List S → ℝ) t = (v : List S → ℝ) (s :: t) := rfl
52 
53 @[simp] theorem branch_history (f : List S → ℝ) (s : S) (h : List S) :
54     branch f s (history f h) = history f (h ++ [s]) := by
55   apply Subtype.ext
56   exact shift_column f s h
57 
58 noncomputable def mass (f : List S → ℝ) : space f →ₗ[ℝ] ℝ :=
59   (LinearMap.proj []).comp (space f).subtype
60 
61 @[simp] theorem mass_apply (f : List S → ℝ) (v : space f) :
62     mass f v = (v : List S → ℝ) [] := rfl
63 
64 @[simp] theorem mass_history (f : List S → ℝ) (h : List S) :
65     mass f (history f h) = f h := by simp
66 
67 /-- The head of a word acts first. -/
68 theorem word_history (f : List S → ℝ) (w h : List S) :
69     wordAction (branch f) w (history f h) = history f (h ++ w) := by
70   induction w generalizing h with
71   | nil => simp
72   | cons s w ih =>
73     simp only [wordAction_cons, LinearMap.comp_apply, branch_history, ih]
74     congr 1
75     simp [List.append_assoc]
76 
77 theorem word_probability (f : List S → ℝ) (w : List S) :
78     mass f (wordAction (branch f) w (history f [])) = f w := by
79   rw [word_history]
80   simp
81 
82 /-- Every coordinate is a declared future-test readout. -/
83 theorem test_evaluation (f : List S → ℝ) (w : List S) (v : space f) :
84     mass f (wordAction (branch f) w v) = (v : List S → ℝ) w := by
85   induction w generalizing v with
86   | nil => rfl
87   | cons s w ih =>
88     change mass f (wordAction (branch f) w (branch f s v)) = _
89     exact ih (branch f s v)
90 
91 /-- A normalized behavior state gives conditional test values. -/
92 theorem conditional_test (f : List S → ℝ) (h t : List S) :
93     mass f (wordAction (branch f) t ((f h)⁻¹ • history f h)) =
94       f (h ++ t) / f h := by
95   rw [map_smul, map_smul, word_history, mass_history]
96   simp [div_eq_mul_inv, mul_comm]
97 
98 theorem conditional_mass (f : List S → ℝ) (h : List S) (hf : f h ≠ 0) :
99     mass f ((f h)⁻¹ • history f h) = 1 := by simp [hf]
100 
101 /-- Equal normalized columns are exactly equal conditional predictions. -/
102 theorem conditional_equivalence (f : List S → ℝ) (h k : List S) :
103     (f h)⁻¹ • history f h = (f k)⁻¹ • history f k ↔
104       ∀ t, f (h ++ t) / f h = f (k ++ t) / f k := by
105   constructor
106   · intro he t
107     have hv := congrArg (fun v : space f => mass f (wordAction (branch f) t v)) he
108     simpa only [conditional_test] using hv
109   · intro he
110     apply Subtype.ext
111     funext t
112     simpa only [Submodule.coe_smul, Pi.smul_apply, history_apply, smul_eq_mul,
113       div_eq_mul_inv, mul_comm] using he t
114 
115 /-- Exact linear models have operators and boundary vectors, not assumed states. -/
116 structure Realization (f : List S → ℝ) (E : Type*) [AddCommGroup E] [Module ℝ E] where
117   initial : E
118   operator : S → E →ₗ[ℝ] E
119   readout : E →ₗ[ℝ] ℝ
120   correct : ∀ w, readout (wordAction operator w initial) = f w
121 
122 noncomputable def canonical (f : List S → ℝ) : Realization f (space f) where
123   initial := history f []
124   operator := branch f
125   readout := mass f
126   correct := word_probability f
127 
128 namespace Realization
129 variable {f : List S → ℝ} {E : Type*} [AddCommGroup E] [Module ℝ E]
130 
131 noncomputable def state (r : Realization f E) (h : List S) : E :=
132   wordAction r.operator h r.initial
133 
134 noncomputable def reachable (r : Realization f E) : Submodule ℝ E :=
135   Submodule.span ℝ (Set.range r.state)
136 
137 def IsReachable (r : Realization f E) : Prop := r.reachable = ⊤
138 
139 noncomputable def observe (r : Realization f E) : E →ₗ[ℝ] (List S → ℝ) :=
140   LinearMap.pi (fun t => r.readout.comp (wordAction r.operator t))
141 
142 def IsObservable (r : Realization f E) : Prop := Function.Injective r.observe
143 
144 @[simp] theorem observe_apply (r : Realization f E) (x : E) (t : List S) :
145     r.observe x t = r.readout (wordAction r.operator t x) := rfl
146 
147 @[simp] theorem observe_state (r : Realization f E) (h : List S) :
148     r.observe (r.state h) = column f h := by
149   funext t
150   simpa only [observe_apply, state, column, wordAction_append, LinearMap.comp_apply]
151     using r.correct (h ++ t)
152 
153 @[simp] theorem observe_operator (r : Realization f E) (s : S) (x : E) :
154     r.observe (r.operator s x) = shift s (r.observe x) := rfl
155 
156 theorem observe_mem (r : Realization f E) (x : E) (hx : x ∈ r.reachable) :
157     r.observe x ∈ space f := by
158   induction hx using Submodule.span_induction with
159   | mem x hx =>
160     obtain ⟨h,rfl⟩ := hx
161     rw [observe_state]
162     exact Submodule.subset_span ⟨h,rfl⟩
163   | zero => simp
164   | add x y hx hy ihx ihy => simpa using (space f).add_mem ihx ihy
165   | smul a x hx ih => simpa using (space f).smul_mem a ih
166 
167 noncomputable def toBehavior (r : Realization f E) : r.reachable →ₗ[ℝ] space f :=
168   (r.observe.domRestrict r.reachable).codRestrict (space f) (fun x => r.observe_mem x x.property)
169 
170 /-- Every behavior vector has a preimage in the reachable part of any realization. -/
171 theorem toBehavior_surjective (r : Realization f E) : Function.Surjective r.toBehavior := by
172   intro v
173   obtain ⟨v,hv⟩ := v
174   have hpre : ∃ x : r.reachable, r.observe x = v := by
175     induction hv using Submodule.span_induction with
176     | mem v hv =>
177       obtain ⟨h,rfl⟩ := hv
178       exact ⟨⟨r.state h,Submodule.subset_span ⟨h,rfl⟩⟩,r.observe_state h⟩
179     | zero => exact ⟨0,map_zero _⟩
180     | add x y hx hy ihx ihy =>
181       obtain ⟨a,ha⟩ := ihx
182       obtain ⟨b,hb⟩ := ihy
183       exact ⟨a+b,by simpa using (map_add r.observe (a : E) (b : E)).trans (congrArg₂ (·+·) ha hb)⟩
184     | smul c x hx ih =>
185       obtain ⟨a,ha⟩ := ih
186       exact ⟨c • a,by simpa using (map_smul r.observe c (a : E)).trans (congrArg (c • ·) ha)⟩
187   obtain ⟨x,hx⟩ := hpre
188   exact ⟨x,Subtype.ext hx⟩
189 
190 /-- The rank of the complete history/test behavior cannot exceed any finite model. -/
191 theorem behavior_dimension_le [FiniteDimensional ℝ E] (r : Realization f E) :
192     Module.finrank ℝ (space f) ≤ Module.finrank ℝ E := by
193   exact (LinearMap.finrank_le_finrank_of_surjective r.toBehavior_surjective).trans
194     (Submodule.finrank_le r.reachable)
195 
196 /-- A reachable observable model is linearly isomorphic to the canonical space. -/
197 noncomputable def equiv (r : Realization f E) (hr : r.IsReachable) (ho : r.IsObservable) :
198     E ≃ₗ[ℝ] space f :=
199   LinearEquiv.ofBijective
200     (r.observe.codRestrict (space f) (fun x => r.observe_mem x (by rw [hr]; trivial)))
201     ⟨fun x y h => ho (congrArg Subtype.val h), by
202       intro v
203       obtain ⟨x,hx⟩ := r.toBehavior_surjective v
204       exact ⟨x, hx⟩⟩
205 
206 @[simp] theorem equiv_apply (r : Realization f E) (hr : r.IsReachable) (ho : r.IsObservable)
207     (x : E) (t : List S) :
208     (r.equiv hr ho x : List S → ℝ) t = r.readout (wordAction r.operator t x) := rfl
209 
210 theorem equiv_initial (r : Realization f E) (hr : r.IsReachable) (ho : r.IsObservable) :
211     r.equiv hr ho r.initial = history f [] := by
212   apply Subtype.ext
213   funext t
214   exact r.correct t
215 
216 theorem equiv_operator (r : Realization f E) (hr : r.IsReachable) (ho : r.IsObservable)
217     (s : S) (x : E) : r.equiv hr ho (r.operator s x) = branch f s (r.equiv hr ho x) := by
218   apply Subtype.ext
219   rfl
220 
221 theorem equiv_mass (r : Realization f E) (hr : r.IsReachable) (ho : r.IsObservable)
222     (x : E) : mass f (r.equiv hr ho x) = r.readout x := rfl
223 
224 end Realization
225 end Komorebi.LSM.Behavior

Back to source controls