StrongRefinement.lean

1 import KomorebiLSM.Normed
2 import Mathlib.Analysis.InnerProductSpace.Projection.Basic
3 
4 /-! P13: strong convergence of compressed bounded operators at each fixed horizon.
5 Uniform operator bounds are used, not operator-norm convergence. -/
6 set_option autoImplicit false
7 open Filter
8 open scoped Topology
9 namespace Komorebi.LSM.Stability
10 universe u v w
11 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
12 variable {X : Type v} [NormedAddCommGroup X] [NormedSpace 𝕜 X]
13 variable {Y : Type w} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]
14 
15 /-- A uniform operator bound permits a strongly convergent family to act on
16 convergent varying vectors. -/
17 theorem strong_apply_varying (A : ℕ → X →L[𝕜] Y) (L : X →L[𝕜] Y)
18     {C : ℝ} (bound : ∀ n, ‖A n‖ ≤ C)
19     (strong : ∀ x, Tendsto (fun n => A n x) atTop (𝓝 (L x)))
20     (x : ℕ → X) (v : X) (hx : Tendsto x atTop (𝓝 v)) :
21     Tendsto (fun n => A n (x n)) atTop (𝓝 (L v)) := by
22   apply tendsto_iff_norm_sub_tendsto_zero.mpr
23   have hbound : ∀ n, ‖A n (x n)-L v‖ ≤
24       C*‖x n-v‖ + ‖A n v-L v‖ := by
25     intro n
26     calc
27       ‖A n (x n)-L v‖ = ‖A n (x n-v)+(A n v-L v)‖ := by
28         rw [map_sub]; congr 1; abel
29       _ ≤ ‖A n (x n-v)‖+‖A n v-L v‖ := norm_add_le _ _
30       _ ≤ C*‖x n-v‖+‖A n v-L v‖ := by
31         apply add_le_add _ le_rfl
32         exact ((A n).le_opNorm _).trans
33           (mul_le_mul_of_nonneg_right (bound n) (norm_nonneg _))
34   have hz : Tendsto (fun n => C*‖x n-v‖+‖A n v-L v‖) atTop (𝓝 0) := by
35     convert (tendsto_const_nhds.mul (tendsto_iff_norm_sub_tendsto_zero.mp hx)).add
36       (tendsto_iff_norm_sub_tendsto_zero.mp (strong v)) using 1; simp
37   exact squeeze_zero (fun n => norm_nonneg _) hbound hz
38 
39 /-- Powers are taken at a fixed finite horizon. -/
40 theorem strong_fixed_powers (A : ℕ → X →L[𝕜] X) (L : X →L[𝕜] X)
41     {C : ℝ} (bound : ∀ n, ‖A n‖ ≤ C)
42     (strong : ∀ x, Tendsto (fun n => A n x) atTop (𝓝 (L x)))
43     (x : X) (k : ℕ) : Tendsto (fun n => ((A n)^k) x) atTop (𝓝 ((L^k) x)) := by
44   induction k with
45   | zero => simp
46   | succ k ih =>
47     have h := strong_apply_varying A L bound strong (fun n => ((A n)^k) x)
48       ((L^k) x) ih
49     simpa only [pow_succ', mul_apply_eq_comp] using h
50 
51 /-- The local consistency estimate for compression. -/
52 theorem compression_error_bound (L P : X →L[𝕜] X) (hP : ‖P‖ ≤ 1) (x : X) :
53     ‖P (L (P x))-L x‖ ≤ ‖L‖*‖P x-x‖+‖P (L x)-L x‖ := by
54   calc
55     ‖P (L (P x))-L x‖ = ‖P (L (P x-x))+(P (L x)-L x)‖ := by
56       simp only [map_sub]; congr 1; abel
57     _ ≤ ‖P (L (P x-x))‖+‖P (L x)-L x‖ := norm_add_le _ _
58     _ ≤ ‖L‖*‖P x-x‖+‖P (L x)-L x‖ := by
59       apply add_le_add _ le_rfl
60       calc
61         ‖P (L (P x-x))‖ ≤ ‖P‖*‖L (P x-x)‖ := P.le_opNorm _
62         _ ≤ 1*‖L (P x-x)‖ := mul_le_mul_of_nonneg_right hP (norm_nonneg _)
63         _ ≤ ‖L‖*‖P x-x‖ := by simpa only [one_mul] using L.le_opNorm (P x-x)
64 
65 theorem compression_uniform_bound (L P : X →L[𝕜] X) (hP : ‖P‖ ≤ 1) :
66     ‖P.comp (L.comp P)‖ ≤ ‖L‖ := by
67   apply ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg L)
68   intro x
69   calc
70     ‖P (L (P x))‖ ≤ ‖P‖*‖L (P x)‖ := P.le_opNorm _
71     _ ≤ 1*‖L (P x)‖ := mul_le_mul_of_nonneg_right hP (norm_nonneg _)
72     _ ≤ ‖L‖*‖x‖ := by
73       simp only [one_mul]
74       apply (L.le_opNorm _).trans
75       apply mul_le_mul_of_nonneg_left _ (norm_nonneg L)
76       exact (P.le_opNorm _).trans (by simpa using mul_le_mul_of_nonneg_right hP (norm_nonneg x))
77 
78 theorem compression_strong (L : X →L[𝕜] X) (P : ℕ → X →L[𝕜] X)
79     (hP : ∀ n, ‖P n‖ ≤ 1)
80     (hstrong : ∀ x, Tendsto (fun n => P n x) atTop (𝓝 x)) (x : X) :
81     Tendsto (fun n => P n (L (P n x))) atTop (𝓝 (L x)) := by
82   apply tendsto_iff_norm_sub_tendsto_zero.mpr
83   have hz : Tendsto (fun n => ‖L‖*‖P n x-x‖+‖P n (L x)-L x‖) atTop (𝓝 0) := by
84     convert (tendsto_const_nhds.mul (tendsto_iff_norm_sub_tendsto_zero.mp (hstrong x))).add
85       (tendsto_iff_norm_sub_tendsto_zero.mp (hstrong (L x))) using 1; simp
86   exact squeeze_zero (fun _ => norm_nonneg _) (fun n => compression_error_bound L (P n) (hP n) x) hz
87 
88 /-- The generalized contraction-family statement includes orthogonal projections. -/
89 theorem contractive_refinement_fixed_horizon (L : X →L[𝕜] X) (P : ℕ → X →L[𝕜] X)
90     (hP : ∀ n, ‖P n‖ ≤ 1)
91     (hstrong : ∀ x, Tendsto (fun n => P n x) atTop (𝓝 x)) (x : X) (k : ℕ) :
92     Tendsto (fun n => (((P n).comp (L.comp (P n)))^k) x) atTop (𝓝 ((L^k) x)) := by
93   exact strong_fixed_powers (fun n => (P n).comp (L.comp (P n))) L
94     (fun n => compression_uniform_bound L (P n) (hP n))
95     (compression_strong L P hP hstrong) x k
96 
97 /-- Additional fitted-operator errors may vanish strongly, provided their own
98 uniform bound is supplied. This is not inferred from a fitting procedure. -/
99 theorem estimated_refinement_fixed_horizon (L : X →L[𝕜] X)
100     (A Ahat : ℕ → X →L[𝕜] X) {C : ℝ}
101     (bound : ∀ n, ‖Ahat n‖ ≤ C)
102     (strong : ∀ x, Tendsto (fun n => A n x) atTop (𝓝 (L x)))
103     (error : ∀ x, Tendsto (fun n => (Ahat n-A n) x) atTop (𝓝 0)) (x : X) (k : ℕ) :
104     Tendsto (fun n => ((Ahat n)^k) x) atTop (𝓝 ((L^k) x)) := by
105   apply strong_fixed_powers Ahat L bound
106   intro y
107   have h := (error y).add (strong y)
108   simpa only [sub_apply, sub_add_cancel, zero_add] using h
109 
110 section Orthogonal
111 variable {𝕜' E : Type*} [RCLike 𝕜'] [NormedAddCommGroup E] [InnerProductSpace 𝕜' E]
112 
113 /-- Actual orthogonal projection maps supply the contraction hypothesis. -/
114 theorem strong_fixed_horizon_refinement (L : E →L[𝕜'] E) (S : ℕ → Submodule 𝕜' E)
115     [∀ n, (S n).HasOrthogonalProjection]
116     (hstrong : ∀ x, Tendsto (fun n => (S n).starProjection x) atTop (𝓝 x))
117     (x : E) (k : ℕ) :
118     Tendsto (fun n => (((S n).starProjection.comp (L.comp (S n).starProjection))^k) x)
119       atTop (𝓝 ((L^k) x)) := by
120   exact contractive_refinement_fixed_horizon L (fun n => (S n).starProjection)
121     (fun n => (S n).starProjection_norm_le) hstrong x k
122 
123 end Orthogonal
124 end Komorebi.LSM.Stability

Back to source controls