DelayClosure.lean

1 import KomorebiLSM.DataSpan
2 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
3 
4 /-! P14: actual finite observation maps and their causal realization. -/
5 set_option autoImplicit false
6 namespace Komorebi.LSM.Delay
7 variable {K X Y : Type*} [Field K]
8 variable [AddCommGroup X] [Module K X] [AddCommGroup Y] [Module K Y]
9 
10 def observation (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ) : X →ₗ[K] (Fin h → Y) :=
11   LinearMap.pi (fun i => C.comp (L ^ i.val))
12 
13 @[simp] theorem observation_apply (C : X →ₗ[K] Y) (L : X →ₗ[K] X)
14     (h : ℕ) (x : X) (i : Fin h) : observation C L h x i = C ((L ^ i.val) x) := rfl
15 
16 theorem mem_observation_kernel (C : X →ₗ[K] Y) (L : X →ₗ[K] X)
17     (h : ℕ) (x : X) : x ∈ LinearMap.ker (observation C L h) ↔
18       ∀ k < h, C ((L ^ k) x) = 0 := by
19   simp only [LinearMap.mem_ker, funext_iff, observation_apply, Pi.zero_apply]
20   constructor
21   · intro hx k hk; exact hx ⟨k,hk⟩
22   · intro hx i; exact hx i.val i.isLt
23 
24 theorem kernel_antitone (C : X →ₗ[K] Y) (L : X →ₗ[K] X) :
25     Antitone (fun h => LinearMap.ker (observation C L h)) := by
26   intro a b hab x hx
27   rw [mem_observation_kernel] at hx ⊢
28   exact fun k hk => hx k (lt_of_lt_of_le hk hab)
29 
30 theorem kernel_closed_iff_plateau (C : X →ₗ[K] Y) (L : X →ₗ[K] X)
31     (h : ℕ) (hh : 0 < h) :
32     LinearMap.ker (observation C L h) ≤ LinearMap.ker ((observation C L h).comp L) ↔
33       LinearMap.ker (observation C L (h+1)) = LinearMap.ker (observation C L h) := by
34   constructor
35   · intro hc
36     apply le_antisymm (kernel_antitone C L (Nat.le_succ h))
37     intro x hx
38     rw [mem_observation_kernel] at hx ⊢
39     intro k hk
40     by_cases kh : k < h
41     · exact hx k kh
42     · have ke : k = h := by omega
43       subst k
44       have hl := hc ((mem_observation_kernel C L h x).mpr hx)
45       change L x ∈ LinearMap.ker (observation C L h) at hl
46       have he := (mem_observation_kernel C L h (L x)).mp hl (h-1) (by omega)
47       rw [← Module.End.mul_apply, ← pow_succ] at he
48       simpa [Nat.sub_add_cancel (by omega : 1 ≤ h)] using he
49   · intro hp x hx
50     change L x ∈ LinearMap.ker (observation C L h)
51     rw [mem_observation_kernel]
52     have hx' := (mem_observation_kernel C L (h+1) x).mp (hp ▸ hx)
53     intro k hk
54     rw [← Module.End.mul_apply, ← pow_succ]
55     exact hx' (k+1) (by omega)
56 
57 
58 theorem kernel_succ (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ) :
59     LinearMap.ker (observation C L (h+1)) =
60       LinearMap.ker C ⊓ (LinearMap.ker (observation C L h)).comap L := by
61   ext x
62   rw [mem_observation_kernel]
63   change (∀ k < h+1, C ((L^k) x) = 0) ↔ C x = 0 ∧
64     L x ∈ LinearMap.ker (observation C L h)
65   rw [mem_observation_kernel]
66   constructor
67   · intro hx
68     refine ⟨?_, ?_⟩
69     · simpa using hx 0 (by omega)
70     · intro k hk
71       rw [← Module.End.mul_apply, ← pow_succ]
72       exact hx (k+1) (by omega)
73   · rintro ⟨hc,hl⟩ k hk
74     cases k with
75     | zero => simpa using hc
76     | succ k =>
77       rw [pow_succ, Module.End.mul_apply]
78       exact hl k (by omega)
79 
80 theorem kernel_stays (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ)
81     (hp : LinearMap.ker (observation C L (h+1)) = LinearMap.ker (observation C L h))
82     (k : ℕ) : LinearMap.ker (observation C L (h+k)) = LinearMap.ker (observation C L h) := by
83   induction k with
84   | zero => simp
85   | succ k ih => rw [Nat.add_succ, kernel_succ, ih, ← kernel_succ, hp]
86 
87 noncomputable def transition (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ)
88     (hc : LinearMap.ker (observation C L h) ≤ LinearMap.ker ((observation C L h).comp L)) :
89     LinearMap.range (observation C L h) →ₗ[K] LinearMap.range (observation C L h) :=
90   (Identification.onRange (observation C L h) ((observation C L h).comp L) hc).codRestrict
91     (LinearMap.range (observation C L h)) (by
92       rintro ⟨y,x,hx⟩
93       subst y
94       rw [show (⟨observation C L h x, _⟩ : LinearMap.range (observation C L h)) =
95         (observation C L h).rangeRestrict x from rfl, Identification.onRange_apply]
96       exact ⟨L x,rfl⟩)
97 
98 @[simp] theorem transition_apply (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ)
99     (hc : LinearMap.ker (observation C L h) ≤ LinearMap.ker ((observation C L h).comp L))
100     (x : X) : transition C L h hc ((observation C L h).rangeRestrict x) =
101       (observation C L h).rangeRestrict (L x) := by
102   apply Subtype.ext
103   exact Identification.onRange_apply _ _ _ _
104 
105 theorem transition_unique (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ)
106     (hc : LinearMap.ker (observation C L h) ≤ LinearMap.ker ((observation C L h).comp L))
107     (D : LinearMap.range (observation C L h) →ₗ[K] LinearMap.range (observation C L h))
108     (hD : ∀ x, D ((observation C L h).rangeRestrict x) = (observation C L h).rangeRestrict (L x)) :
109     D = transition C L h hc := by
110   apply LinearMap.ext
111   rintro ⟨y,x,hx⟩
112   subst y
113   exact (hD x).trans (transition_apply C L h hc x).symm
114 
115 theorem transition_exists_iff (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ) :
116     (∃ D : LinearMap.range (observation C L h) →ₗ[K] LinearMap.range (observation C L h),
117       ∀ x, D ((observation C L h).rangeRestrict x) = (observation C L h).rangeRestrict (L x)) ↔
118     LinearMap.ker (observation C L h) ≤ LinearMap.ker ((observation C L h).comp L) := by
119   constructor
120   · rintro ⟨D,hD⟩ x hx
121     have he := hD x
122     have hz : (observation C L h).rangeRestrict x = 0 := Subtype.ext hx
123     rw [hz, map_zero] at he
124     exact (congrArg Subtype.val he).symm
125   · intro hc
126     exact ⟨transition C L h hc, transition_apply C L h hc⟩
127 
128 theorem transition_iterates (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ)
129     (hc : LinearMap.ker (observation C L h) ≤ LinearMap.ker ((observation C L h).comp L))
130     (k : ℕ) (x : X) : (transition C L h hc ^ k) ((observation C L h).rangeRestrict x) =
131       (observation C L h).rangeRestrict ((L^k) x) := by
132   induction k with
133   | zero => rfl
134   | succ k ih => rw [pow_succ', Module.End.mul_apply, ih, transition_apply,
135       pow_succ', Module.End.mul_apply]
136 
137 /-- The window starting at s is available at s+h-1; its last block is that current output. -/
138 theorem causal_last_block (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ) (hh : 0 < h)
139     (s : ℕ) (x : X) : observation C L h ((L^s) x) ⟨h-1,by omega⟩ =
140       C ((L^(s+h-1)) x) := by
141   rw [observation_apply, ← Module.End.mul_apply, ← pow_add]
142   have he : h - 1 + s = s + h - 1 := by omega
143   rw [he]
144 
145 variable [FiniteDimensional K X]
146 
147 theorem rank_plateau_iff_kernel (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ) :
148     Module.finrank K (LinearMap.range (observation C L (h+1))) =
149       Module.finrank K (LinearMap.range (observation C L h)) ↔
150     LinearMap.ker (observation C L (h+1)) = LinearMap.ker (observation C L h) := by
151   have ha := (observation C L h).finrank_range_add_finrank_ker
152   have hb := (observation C L (h+1)).finrank_range_add_finrank_ker
153   constructor
154   · intro hr
155     apply Submodule.eq_of_le_of_finrank_eq (kernel_antitone C L (Nat.le_succ h))
156     change Module.finrank K (LinearMap.ker (observation C L (h+1))) = Module.finrank K (LinearMap.ker (observation C L h))
157     omega
158   · intro hk
159     have he := congrArg (fun W : Submodule K X => Module.finrank K W) hk
160     omega
161 
162 theorem dimension_closure (C : X →ₗ[K] Y) (L : X →ₗ[K] X)
163     (d : ℕ) (hd : Module.finrank K X ≤ d) :
164     LinearMap.ker (observation C L (d+1)) = LinearMap.ker (observation C L d) := by
165   classical
166   have hex : ∃ n ≤ d, LinearMap.ker (observation C L (n+1)) =
167       LinearMap.ker (observation C L n) := by
168     by_contra hn
169     push Not at hn
170     have hg : ∀ n ≤ d+1, Module.finrank K (LinearMap.ker (observation C L n)) + n ≤
171         Module.finrank K X := by
172       intro n
173       induction n with
174       | zero => intro _; simpa using (LinearMap.ker (observation C L 0)).finrank_le
175       | succ n ih =>
176         intro hnd
177         have hi := ih (by omega)
178         have hs := Submodule.finrank_lt_finrank_of_lt
179           (lt_of_le_of_ne (kernel_antitone C L (Nat.le_succ n)) (hn n (by omega)))
180         change Module.finrank K (LinearMap.ker (observation C L (n+1))) < Module.finrank K (LinearMap.ker (observation C L n)) at hs
181         omega
182     have := hg (d+1) (by omega)
183     omega
184   obtain ⟨n,hn,hp⟩ := hex
185   have h1 := kernel_stays C L n hp (d+1-n)
186   have h0 := kernel_stays C L n hp (d-n)
187   rw [Nat.add_sub_of_le (by omega : n ≤ d+1)] at h1
188   rw [Nat.add_sub_of_le hn] at h0
189   exact h1.trans h0.symm
190 
191 theorem delay_closure_rank_iff (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ) (hh : 0 < h) :
192     (∃ D : LinearMap.range (observation C L h) →ₗ[K] LinearMap.range (observation C L h),
193       ∀ x, D ((observation C L h).rangeRestrict x) = (observation C L h).rangeRestrict (L x)) ↔
194     Module.finrank K (LinearMap.range (observation C L (h+1))) =
195       Module.finrank K (LinearMap.range (observation C L h)) := by
196   rw [transition_exists_iff, kernel_closed_iff_plateau C L h hh, rank_plateau_iff_kernel]
197 
198 omit [FiniteDimensional K X] in
199 theorem causal_future_output (C : X →ₗ[K] Y) (L : X →ₗ[K] X) (h : ℕ) (hh : 0 < h)
200     (hc : LinearMap.ker (observation C L h) ≤ LinearMap.ker ((observation C L h).comp L))
201     (s k : ℕ) (x : X) :
202     ((transition C L h hc ^ k) ((observation C L h).rangeRestrict ((L^s) x))).val ⟨h-1,by omega⟩ =
203       C ((L^(s+k+h-1)) x) := by
204   rw [transition_iterates]
205   change observation C L h ((L^k) ((L^s) x)) ⟨h-1,by omega⟩ = _
206   rw [← Module.End.mul_apply, ← pow_add, causal_last_block C L h hh]
207   have he : k + s + h - 1 = s + k + h - 1 := by omega
208   rw [he]
209 end Komorebi.LSM.Delay

Back to source controls