MemoryStability.lean

1 import KomorebiLSM.MemoryBounds
2 import KomorebiLSM.DefectPropagation
3 
4 /-! P19: the finite-memory predictor is evaluated on its own recursively
5 computed history. Integer indices retain explicit initialization. -/
6 set_option autoImplicit false
7 open scoped BigOperators
8 namespace Komorebi.LSM.Stability
9 universe u v
10 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
11 variable {X : Type v} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
12 
13 /-- The finite-memory transition before any added, shared forcing. -/
14 def finiteMemory (A : X →L[𝕜] X) (K : ℕ → X →L[𝕜] X) (H : ℕ)
15     (z : ℤ → X) (t : ℤ) : X := A (z t)+∑ k ∈ Finset.range H, K k (z (t-1-(k:ℤ)))
16 
17 noncomputable def memoryGain (A : X →L[𝕜] X) (K : ℕ → X →L[𝕜] X) (H : ℕ) : ℝ :=
18   ‖A‖+∑ k ∈ Finset.range H, ‖K k‖
19 
20 theorem memoryGain_nonneg (A : X →L[𝕜] X) (K : ℕ → X →L[𝕜] X) (H : ℕ) :
21     0 ≤ memoryGain A K H :=
22   add_nonneg (norm_nonneg _) (Finset.sum_nonneg (fun _ _ => norm_nonneg _))
23 
24 theorem finiteMemory_sub (A : X →L[𝕜] X) (K : ℕ → X →L[𝕜] X) (H : ℕ)
25     (z w : ℤ → X) (t : ℤ) :
26     finiteMemory A K H z t-finiteMemory A K H w t =
27       A (z t-w t)+∑ k ∈ Finset.range H, K k (z (t-1-(k:ℤ))-w (t-1-(k:ℤ))) := by
28   simp only [finiteMemory, map_sub, Finset.sum_sub_distrib]
29   abel
30 
31 theorem finiteMemory_error_bound (A : X →L[𝕜] X) (K : ℕ → X →L[𝕜] X)
32     (H : ℕ) (z w : ℤ → X) (t : ℤ) {E : ℝ}
33     (window : ∀ s, t-(H:ℤ) ≤ s → s ≤ t → ‖z s-w s‖ ≤ E) :
34     ‖finiteMemory A K H z t-finiteMemory A K H w t‖ ≤ memoryGain A K H*E := by
35   rw [finiteMemory_sub]
36   calc
37     ‖A (z t-w t)+∑ k ∈ Finset.range H, K k (z (t-1-(k:ℤ))-w (t-1-(k:ℤ)))‖ ≤
38         ‖A (z t-w t)‖+∑ k ∈ Finset.range H, ‖K k (z (t-1-(k:ℤ))-w (t-1-(k:ℤ)))‖ :=
39       (norm_add_le _ _).trans (add_le_add le_rfl (norm_sum_le _ _))
40     _ ≤ ‖A‖*E+∑ k ∈ Finset.range H, ‖K k‖*E := by
41       apply add_le_add
42       · exact (A.le_opNorm _).trans
43           (mul_le_mul_of_nonneg_left (window t (by omega) le_rfl) (norm_nonneg A))
44       · apply Finset.sum_le_sum
45         intro k hk
46         have hk' := Finset.mem_range.mp hk
47         exact ((K k).le_opNorm _).trans (mul_le_mul_of_nonneg_left
48           (window _ (by omega) (by omega)) (norm_nonneg _))
49     _ = _ := by rw [memoryGain, add_mul, Finset.sum_mul]
50 
51 /-- The common invariant error radius, including the initial window. -/
52 theorem invariant_error_radius {a E0 D : ℝ} (ha : a < 1) (hE0 : 0 ≤ E0) :
53     let E := max E0 (D/(1-a))
54     0 ≤ E ∧ E0 ≤ E ∧ a*E+D ≤ E := by
55   dsimp
56   have hd : D ≤ max E0 (D/(1-a))*(1-a) :=
57     (div_le_iff₀ (sub_pos.mpr ha)).mp (le_max_right _ _)
58   exact ⟨hE0.trans (le_max_left _ _), le_max_left _ _, by nlinarith⟩
59 
60 /-- Defects are evaluated on the true history; the conclusion concerns the
61 approximate recurrence's own history, including its separate initialization. -/
62 theorem finite_memory_prediction_bound (A : X →L[𝕜] X) (K : ℕ → X →L[𝕜] X)
63     (H : ℕ) (z w : ℤ → X) (g : ℕ → X) {D E0 : ℝ}
64     (stable : memoryGain A K H < 1) (hE0 : 0 ≤ E0)
65     (initial : ∀ s : ℤ, -(H:ℤ) ≤ s → s ≤ 0 → ‖z s-w s‖ ≤ E0)
66     (pred_step : ∀ t : ℕ, w ((t:ℤ)+1)=finiteMemory A K H w t+g t)
67     (defect : ∀ t : ℕ, ‖z ((t:ℤ)+1)-(finiteMemory A K H z t+g t)‖ ≤ D)
68     (T : ℕ) :
69     ‖z T-w T‖ ≤ max E0 (D/(1-memoryGain A K H)) := by
70   let E := max E0 (D/(1-memoryGain A K H))
71   obtain ⟨_, hinit, hinv⟩ := invariant_error_radius stable hE0
72   have invariant : ∀ t : ℕ, ∀ s : ℤ, -(H:ℤ) ≤ s → s ≤ (t:ℤ) → ‖z s-w s‖ ≤ E := by
73     intro t
74     induction t with
75     | zero =>
76       intro s hs ht
77       exact (initial s hs (by simpa using ht)).trans hinit
78     | succ t ih =>
79       intro s hs ht
80       by_cases hold : s ≤ (t:ℤ)
81       · exact ih s hs hold
82       · have heq : s=(t:ℤ)+1 := by omega
83         rw [heq, pred_step]
84         have hmem := finiteMemory_error_bound A K H z w (t:ℤ)
85           (fun j hj htop => ih j (by omega) htop)
86         have htri := norm_add_le
87           (z ((t:ℤ)+1)-(finiteMemory A K H z t+g t))
88           (finiteMemory A K H z t-finiteMemory A K H w t)
89         have hid : (z ((t:ℤ)+1)-(finiteMemory A K H z t+g t))+
90             (finiteMemory A K H z t-finiteMemory A K H w t) =
91             z ((t:ℤ)+1)-(finiteMemory A K H w t+g t) := by abel
92         rw [hid] at htri
93         exact (htri.trans (add_le_add (defect t) hmem)).trans
94           (by dsimp [E] at *; linarith)
95   exact invariant T T (by omega) le_rfl
96 
97 /-- The pointwise result yields the stated supremum over nonnegative time. -/
98 theorem finite_memory_uniform_prediction_bound (A : X →L[𝕜] X)
99     (K : ℕ → X →L[𝕜] X) (H : ℕ) (z w : ℤ → X) (g : ℕ → X) {D E0 : ℝ}
100     (stable : memoryGain A K H < 1) (hE0 : 0 ≤ E0)
101     (initial : ∀ s : ℤ, -(H:ℤ) ≤ s → s ≤ 0 → ‖z s-w s‖ ≤ E0)
102     (pred_step : ∀ t : ℕ, w ((t:ℤ)+1)=finiteMemory A K H w t+g t)
103     (defect : ∀ t : ℕ, ‖z ((t:ℤ)+1)-(finiteMemory A K H z t+g t)‖ ≤ D) :
104     sSup (Set.range (fun t : ℕ => ‖z t-w t‖)) ≤ max E0 (D/(1-memoryGain A K H)) := by
105   apply csSup_le (Set.range_nonempty _)
106   rintro _ ⟨t, rfl⟩
107   exact finite_memory_prediction_bound A K H z w g stable hE0 initial pred_step defect t
108 
109 end Komorebi.LSM.Stability

Back to source controls