DefectPropagation.lean

1 import KomorebiLSM.Normed
2 import Mathlib.Algebra.BigOperators.Intervals
3 import Mathlib.Algebra.Field.GeomSum
4 import Mathlib.Topology.MetricSpace.Lipschitz
5 import Mathlib.Tactic.Ring
6 import Mathlib.Tactic.FieldSimp
7 
8 /-! P18: actual time-dependent trajectory defects and their propagated bounds. -/
9 set_option autoImplicit false
10 open scoped BigOperators
11 namespace Komorebi.LSM.Stability
12 
13 /-- The exact scalar envelope, written with the manuscript's suffix products. -/
14 def errorEnvelope (l d : ℕ → ℝ) (e0 : ℝ) (T : ℕ) : ℝ :=
15   (∏ j ∈ Finset.range T, l j) * e0 +
16     ∑ k ∈ Finset.range T, (∏ j ∈ Finset.Ico (k+1) T, l j) * d k
17 
18 @[simp] theorem errorEnvelope_zero (l d : ℕ → ℝ) (e0 : ℝ) :
19     errorEnvelope l d e0 0 = e0 := by simp [errorEnvelope]
20 
21 theorem errorEnvelope_succ (l d : ℕ → ℝ) (e0 : ℝ) (T : ℕ) :
22     errorEnvelope l d e0 (T+1) = l T * errorEnvelope l d e0 T + d T := by
23   rw [errorEnvelope, Finset.prod_range_succ, Finset.sum_range_succ]
24   have hsum :
25       (∑ k ∈ Finset.range T, (∏ j ∈ Finset.Ico (k+1) (T+1), l j) * d k) =
26       l T * (∑ k ∈ Finset.range T, (∏ j ∈ Finset.Ico (k+1) T, l j) * d k) := by
27     rw [Finset.mul_sum]
28     apply Finset.sum_congr rfl
29     intro k hk
30     rw [Finset.prod_Ico_succ_top (by simpa using Finset.mem_range.mp hk)]
31     ring
32   rw [hsum]
33   simp only [Finset.Ico_self, Finset.prod_empty, one_mul]
34   unfold errorEnvelope
35   ring
36 
37 theorem recurrence_product_sum (e l d : ℕ → ℝ) (hl : ∀ t, 0 ≤ l t)
38     (step : ∀ t, e (t+1) ≤ l t * e t + d t) (T : ℕ) :
39     e T ≤ errorEnvelope l d (e 0) T := by
40   induction T with
41   | zero => simp
42   | succ T ih =>
43     rw [errorEnvelope_succ]
44     exact (step T).trans (add_le_add (mul_le_mul_of_nonneg_left ih (hl T)) le_rfl)
45 
46 /-- The one-step inequality follows from a true local residual and the two
47 actual inputs to the approximate step. -/
48 theorem local_error_step {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F]
49     (f : E → F) (x y : E) (next : F) {l d : ℝ}
50     (defect : ‖next - f x‖ ≤ d) (lip : ‖f x - f y‖ ≤ l * ‖x-y‖) :
51     ‖next - f y‖ ≤ l * ‖x-y‖ + d := by
52   have ht := norm_add_le (next-f x) (f x-f y)
53   have hid : (next-f x)+(f x-f y)=next-f y := by abel
54   rw [hid] at ht
55   linarith
56 
57 universe u v
58 /-- State spaces may change at every time. The domain membership and Lipschitz
59 assumptions are not inferred from a small initial error. -/
60 theorem compositional_defect_propagation {X : Type u} {Z : ℕ → Type v}
61     [∀ t, NormedAddCommGroup (Z t)]
62     (gamma : (t : ℕ) → X → Z t) (F : ℕ → X → X)
63     (f : (t : ℕ) → Z t → Z (t+1)) (x : ℕ → X) (zhat : (t : ℕ) → Z t)
64     (domain : (t : ℕ) → Set (Z t)) (l : ℕ → NNReal) (d : ℕ → ℝ)
65     (true_step : ∀ t, x (t+1)=F t (x t))
66     (pred_step : ∀ t, zhat (t+1)=f t (zhat t))
67     (true_mem : ∀ t, gamma t (x t) ∈ domain t)
68     (pred_mem : ∀ t, zhat t ∈ domain t)
69     (lip : ∀ t, LipschitzOnWith (l t) (f t) (domain t))
70     (defect : ∀ t, ‖gamma (t+1) (F t (x t))-f t (gamma t (x t))‖ ≤ d t)
71     (T : ℕ) :
72     ‖gamma T (x T)-zhat T‖ ≤
73       errorEnvelope (fun t => (l t : ℝ)) d ‖gamma 0 (x 0)-zhat 0‖ T := by
74   apply recurrence_product_sum (fun t => ‖gamma t (x t)-zhat t‖)
75     (fun t => (l t : ℝ)) d (fun t => (l t).coe_nonneg)
76   intro t
77   rw [true_step, pred_step]
78   apply local_error_step _ _ _ _ (defect t)
79   simpa only [dist_eq_norm] using (lip t).dist_le_mul (gamma t (x t)) (true_mem t) (zhat t) (pred_mem t)
80 
81 theorem decoder_error_bound {E F : Type*} [NormedAddCommGroup E] [NormedAddCommGroup F]
82     (H : E → F) (x y : E) (output : F) {k eta : ℝ}
83     (residual : ‖output-H x‖ ≤ eta) (lip : ‖H x-H y‖ ≤ k*‖x-y‖) :
84     ‖output-H y‖ ≤ eta+k*‖x-y‖ := by
85   simpa only [add_comm] using local_error_step H x y output residual lip
86 
87 theorem constant_gain_bound (e : ℕ → ℝ) {rho delta : ℝ}
88     (hrho : 0 ≤ rho) (hsmall : rho < 1)
89     (step : ∀ t, e (t+1) ≤ rho*e t+delta) (T : ℕ) :
90     e T ≤ rho^T*e 0 + delta*((1-rho^T)/(1-rho)) := by
91   have hden : 1-rho ≠ 0 := ne_of_gt (sub_pos.mpr hsmall)
92   induction T with
93   | zero => simp
94   | succ T ih =>
95     calc
96       e (T+1) ≤ rho*e T+delta := step T
97       _ ≤ rho*(rho^T*e 0+delta*((1-rho^T)/(1-rho)))+delta :=
98         add_le_add (mul_le_mul_of_nonneg_left ih hrho) le_rfl
99       _ = _ := by rw [pow_succ']; field_simp; ring
100 
101 /-- The separation of representational and fitted-operator defects is literal
102 linear-map algebra. -/
103 theorem linear_defect_split {𝕜 E G : Type*} [CommRing 𝕜]
104     [AddCommGroup E] [Module 𝕜 E] [AddCommGroup G] [Module 𝕜 G]
105     (R : E →ₗ[𝕜] G) (L : E →ₗ[𝕜] E) (B Bhat : G →ₗ[𝕜] G) :
106     R.comp L-Bhat.comp R = (R.comp L-B.comp R)+(B-Bhat).comp R := by
107   ext x
108   simp only [LinearMap.sub_apply, LinearMap.add_apply, LinearMap.comp_apply]
109   abel
110 
111 end Komorebi.LSM.Stability

Back to source controls