FilteringStability.lean

1 import KomorebiLSM.IdentificationBound
2 import KomorebiLSM.DefectPropagation
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.Filtering
6 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
7 
8 /-- Normalization is only used below with positive mass. -/
9 noncomputable def normalize (lam : E →L[ℝ] ℝ) (u : E) : E := (lam u)⁻¹ • u
10 
11 theorem prediction_error (B Bhat : E →L[ℝ] E) (z zhat : E)
12     (L ε R : ℝ) (hL : ‖Bhat‖ ≤ L) (hε : ‖Bhat-B‖ ≤ ε) (hR : ‖z‖ ≤ R) :
13     ‖Bhat zhat - B z‖ ≤ L * ‖zhat-z‖ + ε * R := by
14   have hε0 : 0 ≤ ε := (norm_nonneg _).trans hε
15   have he : Bhat zhat - B z = Bhat (zhat-z) + (Bhat-B) z := by simp
16   rw [he]
17   calc
18     _ ≤ ‖Bhat (zhat-z)‖ + ‖(Bhat-B) z‖ := norm_add_le _ _
19     _ ≤ ‖Bhat‖ * ‖zhat-z‖ + ‖Bhat-B‖ * ‖z‖ := add_le_add (Bhat.le_opNorm _) ((Bhat-B).le_opNorm _)
20     _ ≤ L * ‖zhat-z‖ + ε * R := add_le_add
21       (mul_le_mul_of_nonneg_right hL (norm_nonneg _))
22       (mul_le_mul hε hR (norm_nonneg _) hε0)
23 
24 theorem mass_lower (lam : E →L[ℝ] ℝ) (u uhat : E) (η D : ℝ)
25     (hp : η ≤ lam u) (hd : ‖uhat-u‖ ≤ D) :
26     η - ‖lam‖ * D ≤ lam uhat := by
27   have h := lam.le_opNorm (uhat-u)
28   have hh := mul_le_mul_of_nonneg_left hd (norm_nonneg lam)
29   rw [map_sub, Real.norm_eq_abs] at h
30   have ha := neg_abs_le (lam uhat-lam u)
31   linarith
32 
33 theorem fitted_mass_positive (lam : E →L[ℝ] ℝ) (u uhat : E) (η D : ℝ)
34     (hp : η ≤ lam u) (hd : ‖uhat-u‖ ≤ D) (hm : ‖lam‖ * D < η) :
35     0 < lam uhat := lt_of_lt_of_le (sub_pos.mpr hm) (mass_lower lam u uhat η D hp hd)
36 
37 theorem normalized_residual (lam : E →L[ℝ] ℝ) (u uhat : E)
38     (hp : lam u ≠ 0) (hq : lam uhat ≠ 0) :
39     normalize lam uhat - normalize lam u =
40       (lam uhat)⁻¹ • ((uhat-u) - (lam (uhat-u)) • normalize lam u) := by
41   unfold normalize
42   rw [map_sub, smul_sub, smul_sub, smul_smul]
43   have hc : (lam uhat)⁻¹ * (lam uhat-lam u) * (lam u)⁻¹ =
44       (lam u)⁻¹ - (lam uhat)⁻¹ := by field_simp
45   rw [smul_smul, hc, sub_smul]
46   abel
47 
48 theorem residual_numerator_bound (lam : E →L[ℝ] ℝ) (z d : E) (R D : ℝ)
49     (hz : ‖z‖ ≤ R) (hd : ‖d‖ ≤ D) :
50     ‖d - (lam d) • z‖ ≤ (1 + R * ‖lam‖) * D := by
51   have hR : 0 ≤ R := (norm_nonneg _).trans hz
52   calc
53     _ ≤ ‖d‖ + ‖(lam d) • z‖ := norm_sub_le _ _
54     _ = ‖d‖ + ‖lam d‖ * ‖z‖ := by rw [norm_smul]
55     _ ≤ ‖d‖ + (‖lam‖ * ‖d‖) * R := add_le_add le_rfl
56       (mul_le_mul (lam.le_opNorm d) hz (norm_nonneg _) (by positivity))
57     _ = (1+R*‖lam‖) * ‖d‖ := by ring
58     _ ≤ _ := mul_le_mul_of_nonneg_left hd (by positivity)
59 
60 theorem normalized_error_checked (lam : E →L[ℝ] ℝ) (u uhat : E) (R D ηhat : ℝ)
61     (hp : lam u ≠ 0) (hq : ηhat ≤ lam uhat) (hη : 0 < ηhat)
62     (hz : ‖normalize lam u‖ ≤ R) (hd : ‖uhat-u‖ ≤ D) :
63     ‖normalize lam uhat - normalize lam u‖ ≤ (1+R*‖lam‖)*D/ηhat := by
64   have hq0 := lt_of_lt_of_le hη hq
65   rw [normalized_residual lam u uhat hp (ne_of_gt hq0), norm_smul,
66     Real.norm_eq_abs, abs_inv, abs_of_pos hq0]
67   have hn := residual_numerator_bound lam (normalize lam u) (uhat-u) R D hz hd
68   calc
69     _ ≤ (lam uhat)⁻¹ * ((1+R*‖lam‖)*D) := mul_le_mul_of_nonneg_left hn (inv_nonneg.mpr hq0.le)
70     _ = ((1+R*‖lam‖)*D) / lam uhat := by rw [div_eq_mul_inv]; ring
71     _ ≤ _ := div_le_div_of_nonneg_left ((norm_nonneg _).trans hn) hη hq
72 
73 theorem normalized_error_margin (lam : E →L[ℝ] ℝ) (u uhat : E) (R D η : ℝ)
74     (hp : η ≤ lam u) (hη : 0 < η) (hz : ‖normalize lam u‖ ≤ R)
75     (hd : ‖uhat-u‖ ≤ D) (hm : ‖lam‖*D < η) :
76     0 < lam uhat ∧
77     ‖normalize lam uhat - normalize lam u‖ ≤ (1+R*‖lam‖)*D/(η-‖lam‖*D) := by
78   exact ⟨fitted_mass_positive lam u uhat η D hp hd hm,
79     normalized_error_checked lam u uhat R D (η-‖lam‖*D)
80       (ne_of_gt (lt_of_lt_of_le hη hp)) (mass_lower lam u uhat η D hp hd)
81       (sub_pos.mpr hm) hz hd⟩
82 
83 theorem filtering_step (lam : E →L[ℝ] ℝ) (B Bhat : E →L[ℝ] E) (z zhat : E)
84     (R L ε ηhat : ℝ) (hL : ‖Bhat‖ ≤ L) (hε : ‖Bhat-B‖ ≤ ε)
85     (hz : ‖z‖ ≤ R) (hzplus : ‖normalize lam (B z)‖ ≤ R)
86     (hp : lam (B z) ≠ 0) (hq : ηhat ≤ lam (Bhat zhat)) (hη : 0 < ηhat) :
87     ‖normalize lam (Bhat zhat) - normalize lam (B z)‖ ≤
88       ((1+R*‖lam‖)*L/ηhat)*‖zhat-z‖ + (1+R*‖lam‖)*ε*R/ηhat := by
89   have h := normalized_error_checked lam (B z) (Bhat zhat) R
90     (L*‖zhat-z‖+ε*R) ηhat hp hq hη hzplus (prediction_error B Bhat z zhat L ε R hL hε hz)
91   convert h using 1; ring
92 
93 theorem filtering_path (lam : E →L[ℝ] ℝ) (B Bhat : ℕ → E →L[ℝ] E)
94     (z zhat : ℕ → E) (R : ℝ) (L ε ηhat : ℕ → ℝ)
95     (true_step : ∀ t, z (t+1) = normalize lam (B t (z t)))
96     (fit_step : ∀ t, zhat (t+1) = normalize lam (Bhat t (zhat t)))
97     (hL : ∀ t, ‖Bhat t‖ ≤ L t) (hε : ∀ t, ‖Bhat t-B t‖ ≤ ε t)
98     (hz : ∀ t, ‖z t‖ ≤ R) (hp : ∀ t, lam (B t (z t)) ≠ 0)
99     (hq : ∀ t, ηhat t ≤ lam (Bhat t (zhat t))) (hη : ∀ t, 0 < ηhat t)
100     (T : ℕ) :
101     ‖zhat T-z T‖ ≤ Stability.errorEnvelope
102       (fun t => (1+R*‖lam‖)*L t/ηhat t)
103       (fun t => (1+R*‖lam‖)*ε t*R/ηhat t) ‖zhat 0-z 0‖ T := by
104   have hR : 0 ≤ R := (norm_nonneg _).trans (hz 0)
105   apply Stability.recurrence_product_sum (fun t => ‖zhat t-z t‖)
106     (fun t => (1+R*‖lam‖)*L t/ηhat t) (fun t => (1+R*‖lam‖)*ε t*R/ηhat t)
107   · intro t
108     have hLt : 0 ≤ L t := (norm_nonneg _).trans (hL t)
109     exact div_nonneg (mul_nonneg (by positivity) hLt) (hη t).le
110   · intro t
111     rw [true_step, fit_step]
112     apply filtering_step lam (B t) (Bhat t) (z t) (zhat t) R (L t) (ε t) (ηhat t)
113       (hL t) (hε t) (hz t) _ (hp t) (hq t) (hη t)
114     rw [← true_step]
115     exact hz (t+1)
116 
117 theorem filtering_uniform (lam : E →L[ℝ] ℝ) (B Bhat : ℕ → E →L[ℝ] E)
118     (z zhat : ℕ → E) (R : ℝ) (L ε ηhat : ℕ → ℝ) (ρ β : ℝ)
119     (true_step : ∀ t, z (t+1) = normalize lam (B t (z t)))
120     (fit_step : ∀ t, zhat (t+1) = normalize lam (Bhat t (zhat t)))
121     (hL : ∀ t, ‖Bhat t‖ ≤ L t) (hε : ∀ t, ‖Bhat t-B t‖ ≤ ε t)
122     (hz : ∀ t, ‖z t‖ ≤ R) (hp : ∀ t, lam (B t (z t)) ≠ 0)
123     (hq : ∀ t, ηhat t ≤ lam (Bhat t (zhat t))) (hη : ∀ t, 0 < ηhat t)
124     (hρ : 0 ≤ ρ) (hsmall : ρ < 1) (hβ : 0 ≤ β)
125     (hα : ∀ t, (1+R*‖lam‖)*L t/ηhat t ≤ ρ)
126     (hforce : ∀ t, (1+R*‖lam‖)*ε t*R/ηhat t ≤ β) (T : ℕ) :
127     ‖zhat T-z T‖ ≤ ρ^T*‖zhat 0-z 0‖ + β/(1-ρ) := by
128   have step : ∀ t, ‖zhat (t+1)-z (t+1)‖ ≤ ρ*‖zhat t-z t‖+β := by
129     intro t
130     rw [true_step, fit_step]
131     have hzplus : ‖normalize lam (B t (z t))‖ ≤ R := by rw [← true_step]; exact hz (t+1)
132     exact (filtering_step lam (B t) (Bhat t) (z t) (zhat t) R (L t) (ε t) (ηhat t)
133       (hL t) (hε t) (hz t) hzplus (hp t) (hq t) (hη t)).trans
134       (add_le_add (mul_le_mul_of_nonneg_right (hα t) (norm_nonneg _)) (hforce t))
135   have h := Stability.constant_gain_bound (fun t => ‖zhat t-z t‖) hρ hsmall step T
136   apply h.trans
137   apply add_le_add le_rfl
138   rw [← mul_div_assoc]
139   apply (div_le_div_iff_of_pos_right (sub_pos.mpr hsmall)).mpr
140   nlinarith [pow_nonneg hρ T]
141 
142 end Komorebi.LSM.Filtering

Back to source controls