Memory.lean

1 import KomorebiLSM.Transfer
2 import KomorebiLSM.LinearClosure
3 import Mathlib.Algebra.BigOperators.Intervals
4 import Mathlib.Tactic.Abel
5 
6 /-! Exact recurrence-elimination component of P10.
7 The geometric tail is proved in MemoryBounds. Recursive rollout error is not claimed here.
8 -/
9 set_option autoImplicit false
10 open scoped BigOperators
11 namespace Komorebi.LSM
12 universe u v w
13 variable {R : Type u} [Ring R]
14 variable {X : Type v} [AddCommGroup X] [Module R X]
15 variable {Y : Type w} [AddCommGroup Y] [Module R Y]
16 
17 /-- Unresolved-state elimination, with the original history index. -/
18 theorem unresolved_solution (C : X →ₗ[R] Y) (D : Y →ₗ[R] Y)
19     (z : ℕ → X) (q : ℕ → Y)
20     (step : ∀ t, q (t+1) = C (z t) + D (q t)) (t : ℕ) :
21     q t = (D^t) (q 0) + ∑ s ∈ Finset.range t, (D^(t-1-s)) (C (z s)) := by
22   induction t with
23   | zero => simp
24   | succ t ih =>
25     rw [step, ih, map_add, map_sum, Finset.sum_range_succ]
26     have hexp : ∀ s ∈ Finset.range t,
27         D ((D^(t-1-s)) (C (z s))) = (D^(t+1-1-s)) (C (z s)) := by
28       intro s hs
29       have hs' := Finset.mem_range.mp hs
30       have hn : t+1-1-s = (t-1-s)+1 := by omega
31       rw [hn, pow_succ']
32       rfl
33     have hsum := Finset.sum_congr rfl hexp
34     rw [hsum]
35     have hpower : D ((D^t) (q 0)) = (D^(t+1)) (q 0) := by
36       rw [pow_succ']; rfl
37     rw [hpower]
38     simp only [Nat.add_sub_cancel, Nat.sub_self, pow_zero, Module.End.one_apply]
39     abel
40 
41 /-- The exact projected history recurrence, without a decay hypothesis. -/
42 theorem exact_memory_history (A : X →ₗ[R] X) (B : Y →ₗ[R] X)
43     (C : X →ₗ[R] Y) (D : Y →ₗ[R] Y) (z : ℕ → X) (q : ℕ → Y)
44     (zstep : ∀ t, z (t+1) = A (z t) + B (q t))
45     (qstep : ∀ t, q (t+1) = C (z t) + D (q t)) (t : ℕ) :
46     z (t+1) = A (z t) +
47       (∑ s ∈ Finset.range t, B ((D^(t-1-s)) (C (z s)))) + B ((D^t) (q 0)) := by
48   rw [zstep, unresolved_solution C D z q qstep, map_add, map_sum]
49   abel
50 
51 /-- The lag-index form printed in P10, including the unresolved initial state. -/
52 theorem exact_memory_lags (A : X →ₗ[R] X) (B : Y →ₗ[R] X)
53     (C : X →ₗ[R] Y) (D : Y →ₗ[R] Y) (z : ℕ → X) (q : ℕ → Y)
54     (zstep : ∀ t, z (t+1) = A (z t) + B (q t))
55     (qstep : ∀ t, q (t+1) = C (z t) + D (q t)) (t : ℕ) :
56     z (t+1) = A (z t) +
57       (∑ k ∈ Finset.range t, B ((D^k) (C (z (t-1-k))))) + B ((D^t) (q 0)) := by
58   rw [exact_memory_history A B C D z q zstep qstep]
59   congr 2
60   have href := Finset.sum_range_reflect
61     (fun s => B ((D^(t-1-s)) (C (z s)))) t
62   calc
63     (∑ s ∈ Finset.range t, B ((D^(t-1-s)) (C (z s)))) =
64         ∑ k ∈ Finset.range t, B ((D^(t-1-(t-1-k))) (C (z (t-1-k)))) := href.symm
65     _ = _ := by
66       apply Finset.sum_congr rfl
67       intro k hk
68       have hkt := Finset.mem_range.mp hk
69       have hn : t-1-(t-1-k) = k := by omega
70       rw [hn]
71 
72 /-- Actual projector blocks give the two coupled recurrences needed above. -/
73 theorem projected_recurrences (P L : X →ₗ[R] X)
74     (idem : ∀ x, P (P x) = P x) (x : ℕ → X)
75     (step : ∀ t, x (t+1) = L (x t)) (t : ℕ) :
76     (P (x (t+1)) = P (L (P (x t))) +
77       P (L (unresolved P (unresolved P (x t))))) ∧
78     (unresolved P (x (t+1)) = unresolved P (L (P (P (x t)))) +
79       unresolved P (L (unresolved P (x t)))) := by
80   rw [step, unresolved_idempotent P idem, idem]
81   constructor
82   · simpa only [closureDefect, LinearMap.comp_apply] using retained_dynamics_split P L (x t)
83   · simp only [unresolved_apply, map_sub]
84     abel
85 
86 /-- P10 specialized to the actual blocks of a single projected transition. -/
87 theorem projected_memory (P L : X →ₗ[R] X)
88     (idem : ∀ x, P (P x) = P x) (x : ℕ → X)
89     (step : ∀ t, x (t+1) = L (x t)) (t : ℕ) :
90     let Q := unresolved P
91     let A := P.comp (L.comp P)
92     let B := P.comp (L.comp Q)
93     let C := Q.comp (L.comp P)
94     let D := Q.comp (L.comp Q)
95     P (x (t+1)) = A (P (x t)) +
96       (∑ k ∈ Finset.range t, B ((D^k) (C (P (x (t-1-k)))))) +
97       B ((D^t) (Q (x 0))) := by
98   dsimp only
99   refine exact_memory_lags (P.comp (L.comp P)) (P.comp (L.comp (unresolved P)))
100     ((unresolved P).comp (L.comp P)) ((unresolved P).comp (L.comp (unresolved P)))
101     (fun s => P (x s)) (fun s => unresolved P (x s)) ?_ ?_ t
102   · intro s
103     have hs := (projected_recurrences P L idem x step s).1
104     simpa only [LinearMap.comp_apply, idem] using hs
105   · intro s
106     have hs := (projected_recurrences P L idem x step s).2
107     simpa only [LinearMap.comp_apply, unresolved_idempotent P idem] using hs
108 
109 end Komorebi.LSM

Back to source controls