MemoryApproximation.lean

1 import KomorebiLSM.MemoryStability
2 
3 /-! The coefficient, tail and initialization budgets used by P19.
4 Zero prehistory and horizons shorter than the memory length are explicit. -/
5 set_option autoImplicit false
6 open scoped BigOperators
7 namespace Komorebi.LSM.Stability
8 universe u v w
9 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
10 variable {X : Type v} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
11 variable {Y : Type w} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
12 
13 def memoryKernel (B : Y →L[𝕜] X) (C : X →L[𝕜] Y) (D : Y →L[𝕜] Y)
14     (k : ℕ) : X →L[𝕜] X := B.comp ((D^k).comp C)
15 
16 /-- Padding a shorter history by zeros has no artificial contribution. -/
17 theorem padded_sum_split (f : ℕ → X) (t H : ℕ) (zero_tail : ∀ k, t ≤ k → f k=0) :
18     (∑ k ∈ Finset.range t, f k) =
19       (∑ k ∈ Finset.range H, f k)+(∑ k ∈ Finset.Ico H t, f k) := by
20   by_cases h : H ≤ t
21   · exact (Finset.sum_range_add_sum_Ico f h).symm
22   · have ht : t ≤ H := by omega
23     rw [Finset.Ico_eq_empty_of_le ht, Finset.sum_empty, add_zero]
24     apply Finset.sum_subset (Finset.range_mono ht)
25     intro k _ hk
26     exact zero_tail k (by simpa only [Finset.mem_range, not_lt] using hk)
27 
28 theorem initialized_memory_split (K : ℕ → X →L[𝕜] X) (z : ℤ → X)
29     (zero_past : ∀ s : ℤ, s < 0 → z s=0) (t H : ℕ) :
30     (∑ k ∈ Finset.range t, K k (z ((t:ℤ)-1-(k:ℤ)))) =
31       (∑ k ∈ Finset.range H, K k (z ((t:ℤ)-1-(k:ℤ))))+
32       (∑ k ∈ Finset.Ico H t, K k (z ((t:ℤ)-1-(k:ℤ)))) := by
33   apply padded_sum_split
34   intro k hk
35   rw [zero_past _ (by omega), map_zero]
36 
37 theorem memory_defect_identity (A Ahat : X →L[𝕜] X)
38     (K Khat : ℕ → X →L[𝕜] X) (z : ℤ → X) (f g : ℕ → X)
39     (zero_past : ∀ s : ℤ, s < 0 → z s=0) (H t : ℕ)
40     (step : z ((t:ℤ)+1)=A (z t)+
41       (∑ k ∈ Finset.range t, K k (z ((t:ℤ)-1-(k:ℤ))))+f t) :
42     z ((t:ℤ)+1)-(finiteMemory Ahat Khat H z t+g t) =
43       (A-Ahat) (z t)+
44       (∑ k ∈ Finset.range H, (K k-Khat k) (z ((t:ℤ)-1-(k:ℤ))))+
45       (∑ k ∈ Finset.Ico H t, K k (z ((t:ℤ)-1-(k:ℤ))))+(f t-g t) := by
46   rw [step, initialized_memory_split K z zero_past t H]
47   simp only [finiteMemory, sub_apply, Finset.sum_sub_distrib]
48   abel
49 
50 theorem bounded_with_zero_prehistory (z : ℤ → X) {Z : ℝ} (hZ : 0 ≤ Z)
51     (zero_past : ∀ s : ℤ, s < 0 → z s=0)
52     (bounded : ∀ s : ℤ, 0 ≤ s → ‖z s‖ ≤ Z) (s : ℤ) : ‖z s‖ ≤ Z := by
53   by_cases hs : 0 ≤ s
54   · exact bounded s hs
55   · rw [zero_past s (lt_of_not_ge hs), norm_zero]
56     exact hZ
57 
58 theorem integer_memory_tail_bound (B : Y →L[𝕜] X) (C : X →L[𝕜] Y)
59     (D : Y →L[𝕜] Y) (z : ℤ → X) {rho Z : ℝ}
60     (hrho : 0 ≤ rho) (hsmall : rho < 1) (hD : ‖D‖ ≤ rho) (hZ : 0 ≤ Z)
61     (bounded : ∀ s, ‖z s‖ ≤ Z) (H t : ℕ) :
62     ‖∑ k ∈ Finset.Ico H t, memoryKernel B C D k (z ((t:ℤ)-1-(k:ℤ)))‖ ≤
63       (‖B‖*‖C‖*Z)*(rho^H/(1-rho)) := by
64   calc
65     ‖∑ k ∈ Finset.Ico H t, memoryKernel B C D k (z ((t:ℤ)-1-(k:ℤ)))‖ ≤
66         ∑ k ∈ Finset.Ico H t, ‖memoryKernel B C D k (z ((t:ℤ)-1-(k:ℤ)))‖ := norm_sum_le _ _
67     _ ≤ ∑ k ∈ Finset.Ico H t, (‖B‖*‖C‖*Z)*rho^k := by
68       apply Finset.sum_le_sum
69       intro k _
70       exact memory_kernel_bound B C D hrho hD _ (bounded _) k
71     _ = (‖B‖*‖C‖*Z)*∑ k ∈ Finset.Ico H t, rho^k := by rw [Finset.mul_sum]
72     _ ≤ _ := mul_le_mul_of_nonneg_left (geometric_interval_bound hrho hsmall H t)
73       (mul_nonneg (mul_nonneg (norm_nonneg _) (norm_nonneg _)) hZ)
74 
75 /-- This is the full Delta formula, with a separately bounded forcing error.
76 It covers H=0 and times t<H, not only a settled memory window. -/
77 theorem memory_approximation_defect_bound (A Ahat : X →L[𝕜] X)
78     (B : Y →L[𝕜] X) (C : X →L[𝕜] Y) (D : Y →L[𝕜] Y)
79     (Khat : ℕ → X →L[𝕜] X) (z : ℤ → X) (f g : ℕ → X)
80     {rho Z F0 : ℝ} (hrho : 0 ≤ rho) (hsmall : rho < 1) (hD : ‖D‖ ≤ rho)
81     (hZ : 0 ≤ Z) (zero_past : ∀ s : ℤ, s < 0 → z s=0)
82     (bounded : ∀ s : ℤ, 0 ≤ s → ‖z s‖ ≤ Z)
83     (forcing : ∀ t, ‖f t-g t‖ ≤ F0) (H t : ℕ)
84     (step : z ((t:ℤ)+1)=A (z t)+
85       (∑ k ∈ Finset.range t, memoryKernel B C D k (z ((t:ℤ)-1-(k:ℤ))))+f t) :
86     ‖z ((t:ℤ)+1)-(finiteMemory Ahat Khat H z t+g t)‖ ≤
87       Z*(‖A-Ahat‖+∑ k ∈ Finset.range H, ‖memoryKernel B C D k-Khat k‖)+
88       (‖B‖*‖C‖*Z)*(rho^H/(1-rho))+F0 := by
89   rw [memory_defect_identity A Ahat (memoryKernel B C D) Khat z f g zero_past H t step]
90   have hz := bounded_with_zero_prehistory z hZ zero_past bounded
91   have hfirst : ‖(A-Ahat) (z t)‖ ≤ ‖A-Ahat‖*Z :=
92     ((A-Ahat).le_opNorm _).trans (mul_le_mul_of_nonneg_left (hz t) (norm_nonneg _))
93   have hcoeff :
94       ‖∑ k ∈ Finset.range H, (memoryKernel B C D k-Khat k) (z ((t:ℤ)-1-(k:ℤ)))‖ ≤
95       (∑ k ∈ Finset.range H, ‖memoryKernel B C D k-Khat k‖)*Z := by
96     apply (norm_sum_le _ _).trans
97     rw [Finset.sum_mul]
98     apply Finset.sum_le_sum
99     intro k _
100     exact ((memoryKernel B C D k-Khat k).le_opNorm _).trans
101       (mul_le_mul_of_nonneg_left (hz _) (norm_nonneg _))
102   have htail := integer_memory_tail_bound B C D z hrho hsmall hD hZ hz H t
103   have hnorm := norm_add_le
104     ((A-Ahat) (z t)+(∑ k ∈ Finset.range H, (memoryKernel B C D k-Khat k) (z ((t:ℤ)-1-(k:ℤ))))+
105       (∑ k ∈ Finset.Ico H t, memoryKernel B C D k (z ((t:ℤ)-1-(k:ℤ))))) (f t-g t)
106   have hnorm2 := norm_add_le
107     ((A-Ahat) (z t)+(∑ k ∈ Finset.range H, (memoryKernel B C D k-Khat k) (z ((t:ℤ)-1-(k:ℤ)))))
108     (∑ k ∈ Finset.Ico H t, memoryKernel B C D k (z ((t:ℤ)-1-(k:ℤ))))
109   have hnorm3 := norm_add_le ((A-Ahat) (z t))
110     (∑ k ∈ Finset.range H, (memoryKernel B C D k-Khat k) (z ((t:ℤ)-1-(k:ℤ))))
111   calc
112     _ ≤ (‖A-Ahat‖*Z+(∑ k ∈ Finset.range H, ‖memoryKernel B C D k-Khat k‖)*Z)+
113         (‖B‖*‖C‖*Z)*(rho^H/(1-rho))+F0 := by linarith [forcing t]
114     _ = _ := by ring
115 
116 theorem discarded_initialized_forcing_bound (B : Y →L[𝕜] X) (D : Y →L[𝕜] Y)
117     {rho : ℝ} (hrho : 0 ≤ rho) (hsmall : rho < 1) (hD : ‖D‖ ≤ rho)
118     (q0 : Y) (t : ℕ) : ‖B ((D^t) q0)-(0 : X)‖ ≤ ‖B‖*‖q0‖ := by
119   rw [sub_zero]
120   apply (unresolved_initial_bound B D hrho hD q0 t).trans
121   calc
122     ‖B‖*rho^t*‖q0‖ ≤ ‖B‖*1*‖q0‖ :=
123       mul_le_mul_of_nonneg_right
124         (mul_le_mul_of_nonneg_left (pow_le_one₀ hrho hsmall.le) (norm_nonneg _)) (norm_nonneg _)
125     _ = _ := by ring
126 
127 /-- Retaining the exact initialization forcing removes its contribution. -/
128 theorem retained_initialized_forcing_bound (f : ℕ → X) (t : ℕ) : ‖f t-f t‖ ≤ (0 : ℝ) := by simp
129 
130 /-- The coefficient/tail budget is inserted into the recursive, not same-history,
131 prediction theorem. -/
132 theorem certified_memory_truncation (A Ahat : X →L[𝕜] X)
133     (B : Y →L[𝕜] X) (C : X →L[𝕜] Y) (D : Y →L[𝕜] Y)
134     (Khat : ℕ → X →L[𝕜] X) (H : ℕ) (z w : ℤ → X) (f g : ℕ → X)
135     {rho Z F0 E0 : ℝ} (hrho : 0 ≤ rho) (hsmall : rho < 1) (hD : ‖D‖ ≤ rho)
136     (hZ : 0 ≤ Z) (hE0 : 0 ≤ E0)
137     (zero_past : ∀ s : ℤ, s < 0 → z s=0)
138     (bounded : ∀ s : ℤ, 0 ≤ s → ‖z s‖ ≤ Z)
139     (forcing : ∀ t, ‖f t-g t‖ ≤ F0)
140     (true_step : ∀ t : ℕ, z ((t:ℤ)+1)=A (z t)+
141       (∑ k ∈ Finset.range t, memoryKernel B C D k (z ((t:ℤ)-1-(k:ℤ))))+f t)
142     (pred_step : ∀ t : ℕ, w ((t:ℤ)+1)=finiteMemory Ahat Khat H w t+g t)
143     (initial : ∀ s : ℤ, -(H:ℤ) ≤ s → s ≤ 0 → ‖z s-w s‖ ≤ E0)
144     (stable : memoryGain Ahat Khat H < 1) :
145     sSup (Set.range (fun t : ℕ => ‖z t-w t‖)) ≤
146       max E0 ((Z*(‖A-Ahat‖+∑ k ∈ Finset.range H, ‖memoryKernel B C D k-Khat k‖)+
147         (‖B‖*‖C‖*Z)*(rho^H/(1-rho))+F0)/(1-memoryGain Ahat Khat H)) := by
148   apply finite_memory_uniform_prediction_bound Ahat Khat H z w g stable hE0 initial pred_step
149   intro t
150   exact memory_approximation_defect_bound A Ahat B C D Khat z f g hrho hsmall hD hZ
151     zero_past bounded forcing H t (true_step t)
152 
153 end Komorebi.LSM.Stability

Back to source controls