MemoryBounds.lean

1 import KomorebiLSM.Normed
2 import KomorebiLSM.Memory
3 import Mathlib.Algebra.Field.GeomSum
4 import Mathlib.Tactic.Ring
5 import Mathlib.Tactic.FieldSimp
6 
7 /-! The one-step memory tail and unresolved-initial-state bounds in P10.
8 These compare right-hand sides on the SAME history. They do not certify
9 recursively generated approximate trajectories.
10 -/
11 set_option autoImplicit false
12 open scoped BigOperators
13 namespace Komorebi.LSM
14 universe u v w
15 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
16 variable {X : Type v} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
17 variable {Y : Type w} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
18 
19 /-- The algebraic memory recurrence transported to continuous linear maps. -/
20 theorem continuous_exact_memory_lags (A : X →L[𝕜] X) (B : Y →L[𝕜] X)
21     (C : X →L[𝕜] Y) (D : Y →L[𝕜] Y) (z : ℕ → X) (q : ℕ → Y)
22     (zstep : ∀ t, z (t+1) = A (z t) + B (q t))
23     (qstep : ∀ t, q (t+1) = C (z t) + D (q t)) (t : ℕ) :
24     z (t+1) = A (z t) +
25       (∑ k ∈ Finset.range t, B ((D^k) (C (z (t-1-k))))) + B ((D^t) (q 0)) := by
26   simpa only [← ContinuousLinearMap.toLinearMap_pow, ContinuousLinearMap.coe_coe]
27     using exact_memory_lags A.toLinearMap B.toLinearMap C.toLinearMap D.toLinearMap
28       z q zstep qstep t
29 
30 theorem iterate_norm_bound (D : Y →L[𝕜] Y) {rho : ℝ}
31     (hrho : 0 ≤ rho) (hD : ‖D‖ ≤ rho) (y : Y) (k : ℕ) :
32     ‖(D^k) y‖ ≤ rho^k * ‖y‖ := by
33   induction k with
34   | zero => simp
35   | succ k ih =>
36     rw [pow_succ', mul_apply_eq_comp]
37     calc
38       ‖D ((D^k) y)‖ ≤ ‖D‖ * ‖(D^k) y‖ := D.le_opNorm _
39       _ ≤ rho * ‖(D^k) y‖ := mul_le_mul_of_nonneg_right hD (norm_nonneg _)
40       _ ≤ rho * (rho^k * ‖y‖) := mul_le_mul_of_nonneg_left ih hrho
41       _ = rho^(k+1) * ‖y‖ := by rw [pow_succ']; ring
42 
43 theorem geometric_interval_bound {rho : ℝ} (hrho : 0 ≤ rho) (hsmall : rho < 1)
44     (H t : ℕ) : (∑ k ∈ Finset.Ico H t, rho^k) ≤ rho^H / (1-rho) := by
45   by_cases hHt : H ≤ t
46   · have hid : (∑ k ∈ Finset.Ico H t, rho^k) * (1-rho) = rho^H-rho^t := by
47       rw [geom_sum_Ico (ne_of_lt hsmall) hHt]
48       have hn : rho-1 ≠ 0 := sub_ne_zero.mpr (ne_of_lt hsmall)
49       field_simp
50       ring
51     apply (le_div_iff₀ (sub_pos.mpr hsmall)).mpr
52     rw [hid]
53     exact sub_le_self _ (pow_nonneg hrho t)
54   · rw [Finset.Ico_eq_empty_of_le (le_of_not_ge hHt)]
55     simp only [Finset.sum_empty]
56     exact div_nonneg (pow_nonneg hrho H) (sub_nonneg.mpr hsmall.le)
57 
58 theorem memory_kernel_bound (B : Y →L[𝕜] X) (C : X →L[𝕜] Y)
59     (D : Y →L[𝕜] Y) {rho Z : ℝ} (hrho : 0 ≤ rho) (hD : ‖D‖ ≤ rho)
60     (z : X) (hz : ‖z‖ ≤ Z) (k : ℕ) :
61     ‖B ((D^k) (C z))‖ ≤ (‖B‖ * ‖C‖ * Z) * rho^k := by
62   calc
63     ‖B ((D^k) (C z))‖ ≤ ‖B‖ * ‖(D^k) (C z)‖ := B.le_opNorm _
64     _ ≤ ‖B‖ * (rho^k * ‖C z‖) :=
65       mul_le_mul_of_nonneg_left (iterate_norm_bound D hrho hD (C z) k) (norm_nonneg B)
66     _ ≤ ‖B‖ * (rho^k * (‖C‖ * ‖z‖)) := by
67       apply mul_le_mul_of_nonneg_left _ (norm_nonneg B)
68       exact mul_le_mul_of_nonneg_left (C.le_opNorm z) (pow_nonneg hrho k)
69     _ ≤ ‖B‖ * (rho^k * (‖C‖ * Z)) := by
70       apply mul_le_mul_of_nonneg_left _ (norm_nonneg B)
71       apply mul_le_mul_of_nonneg_left _ (pow_nonneg hrho k)
72       exact mul_le_mul_of_nonneg_left hz (norm_nonneg C)
73     _ = _ := by ring
74 
75 theorem memory_tail_bound (B : Y →L[𝕜] X) (C : X →L[𝕜] Y)
76     (D : Y →L[𝕜] Y) {rho Z : ℝ} (hrho : 0 ≤ rho) (hsmall : rho < 1)
77     (hD : ‖D‖ ≤ rho) (hZ : 0 ≤ Z) (z : ℕ → X) (H t : ℕ)
78     (bounded : ∀ k ∈ Finset.Ico H t, ‖z (t-1-k)‖ ≤ Z) :
79     ‖∑ k ∈ Finset.Ico H t, B ((D^k) (C (z (t-1-k))))‖ ≤
80       (‖B‖ * ‖C‖ * Z) * (rho^H / (1-rho)) := by
81   calc
82     ‖∑ k ∈ Finset.Ico H t, B ((D^k) (C (z (t-1-k))))‖ ≤
83         ∑ k ∈ Finset.Ico H t, ‖B ((D^k) (C (z (t-1-k))))‖ := norm_sum_le _ _
84     _ ≤ ∑ k ∈ Finset.Ico H t, (‖B‖ * ‖C‖ * Z) * rho^k := by
85       apply Finset.sum_le_sum
86       intro k hk
87       exact memory_kernel_bound B C D hrho hD _ (bounded k hk) k
88     _ = (‖B‖ * ‖C‖ * Z) * ∑ k ∈ Finset.Ico H t, rho^k := by rw [Finset.mul_sum]
89     _ ≤ _ := mul_le_mul_of_nonneg_left (geometric_interval_bound hrho hsmall H t)
90       (mul_nonneg (mul_nonneg (norm_nonneg B) (norm_nonneg C)) hZ)
91 
92 /-- Actual full-minus-truncated memory sum, evaluated on one fixed history. -/
93 theorem memory_truncation_difference_bound (B : Y →L[𝕜] X) (C : X →L[𝕜] Y)
94     (D : Y →L[𝕜] Y) {rho Z : ℝ} (hrho : 0 ≤ rho) (hsmall : rho < 1)
95     (hD : ‖D‖ ≤ rho) (hZ : 0 ≤ Z) (z : ℕ → X) (H t : ℕ) (hHt : H ≤ t)
96     (bounded : ∀ k ∈ Finset.Ico H t, ‖z (t-1-k)‖ ≤ Z) :
97     ‖(∑ k ∈ Finset.range t, B ((D^k) (C (z (t-1-k))))) -
98       (∑ k ∈ Finset.range H, B ((D^k) (C (z (t-1-k)))))‖ ≤
99       (‖B‖ * ‖C‖ * Z) * (rho^H / (1-rho)) := by
100   rw [← Finset.sum_Ico_eq_sub (fun k => B ((D^k) (C (z (t-1-k))))) hHt]
101   exact memory_tail_bound B C D hrho hsmall hD hZ z H t bounded
102 
103 theorem unresolved_initial_bound (B : Y →L[𝕜] X) (D : Y →L[𝕜] Y)
104     {rho : ℝ} (hrho : 0 ≤ rho) (hD : ‖D‖ ≤ rho) (q0 : Y) (t : ℕ) :
105     ‖B ((D^t) q0)‖ ≤ ‖B‖ * rho^t * ‖q0‖ := by
106   calc
107     ‖B ((D^t) q0)‖ ≤ ‖B‖ * ‖(D^t) q0‖ := B.le_opNorm _
108     _ ≤ ‖B‖ * (rho^t * ‖q0‖) :=
109       mul_le_mul_of_nonneg_left (iterate_norm_bound D hrho hD q0 t) (norm_nonneg B)
110     _ = _ := by ring
111 
112 end Komorebi.LSM

Back to source controls