CascadeLimits.lean

1 import KomorebiSpace.CascadeProjections
2 import Mathlib.Analysis.Normed.Group.InfiniteSum
3 import Mathlib.Analysis.SpecificLimits.Basic
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Infinite reconstruction and the persistent coarse component
9 
10 Natural-order partial sums are used unless absolute summability is explicitly
11 assumed. No unconditional `HasSum` claim is inferred merely from ordered
12 convergence. Coarse data must be lifted before their size is tested.
13 -/
14 universe u v
15 noncomputable section
16 namespace KomorebiSpace
17 namespace CoarseningCascade
18 open Filter
19 open scoped Topology
20 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
21 variable (T : CoarseningCascade.{u,v} 𝕜)
22 
23 @[simp] theorem partial_error (x : T.Obj 0) (N : ℕ) :
24     ‖x - T.reconstructed N x‖ = ‖T.remainder N x‖ := by
25   rw [partial_apply, sub_sub_cancel]
26 
27 /-- The exact convergence criterion, with no summability assumption. -/
28 theorem partial_tendsto_iff (x : T.Obj 0) :
29     Tendsto (fun N => T.reconstructed N x) atTop (𝓝 x) ↔
30     Tendsto (fun N => T.remainder N x) atTop (𝓝 0) := by
31   constructor
32   · intro h
33     have hh := (tendsto_const_nhds (x := x)).sub h
34     simpa only [partial_apply, sub_sub_cancel, sub_self] using hh
35   · intro h
36     have hh := (tendsto_const_nhds (x := x)).sub h
37     simpa only [partial_apply, sub_zero] using hh
38 
39 /-- The finite theorem upgrades to ordered infinite reconstruction precisely
40 when its actual lifted remainder vanishes. -/
41 theorem ordered_reconstruction_iff (x : T.Obj 0) :
42     Tendsto (fun N => ∑ n ∈ Finset.range N, T.detailTerm x n) atTop (𝓝 x) ↔
43     Tendsto (fun N => T.remainder N x) atTop (𝓝 0) := by
44   simpa only [partial_eq_sum] using T.partial_tendsto_iff x
45 
46 /-- Recoverable data form a linear subspace, not necessarily the entire space. -/
47 def recoverable : Submodule 𝕜 (T.Obj 0) where
48   carrier := {x | Tendsto (fun N => T.remainder N x) atTop (𝓝 0)}
49   zero_mem' := by simpa only [Set.mem_ofPred_eq, map_zero] using (tendsto_const_nhds (x := (0 : T.Obj 0)))
50   add_mem' := by
51     intro x y hx hy
52     simpa only [Set.mem_ofPred_eq, map_add, zero_add] using hx.add hy
53   smul_mem' := by
54     intro c x hx
55     simpa only [Set.mem_ofPred_eq, map_smul, smul_zero] using (tendsto_const_nhds (x := c)).smul hx
56 
57 @[simp] theorem mem_recoverable (x : T.Obj 0) :
58     x ∈ T.recoverable ↔ Tendsto (fun N => T.remainder N x) atTop (𝓝 0) := Iff.rfl
59 
60 /-- The persistent and recoverable subspaces intersect only at zero. -/
61 theorem persistent_recoverable_zero (x : T.Obj 0)
62     (hp : x ∈ T.persistent) (hr : x ∈ T.recoverable) : x = 0 := by
63   change ∀ n, T.remainder n x = x at hp
64   have h : Tendsto (fun _ : ℕ => x) atTop (𝓝 0) := by
65     change Tendsto (fun N => T.remainder N x) atTop (𝓝 0) at hr
66     simpa only [hp] using hr
67   exact tendsto_nhds_unique tendsto_const_nhds h
68 
69 theorem zero_iff_details_on_recoverable (x : T.Obj 0) (hx : x ∈ T.recoverable) :
70     x = 0 ↔ ∀ n, T.detail x n = 0 := by
71   constructor
72   · rintro rfl; exact T.detail_zero
73   · intro h
74     exact T.persistent_recoverable_zero x ((T.persistent_iff_details_zero x).2 h) hx
75 
76 /-- All detail coordinates are injective on the recoverable subspace. -/
77 theorem details_injective_on_recoverable (x y : T.Obj 0)
78     (hx : x ∈ T.recoverable) (hy : y ∈ T.recoverable)
79     (hd : ∀ n, T.detail x n = T.detail y n) : x = y := by
80   apply sub_eq_zero.mp
81   exact T.persistent_recoverable_zero (x-y)
82     ((T.equal_details_iff_persistent_difference x y).1 hd)
83     (T.recoverable.sub_mem hx hy)
84 
85 /-- Every convergent remainder lands in the persistent coarse subspace. -/
86 theorem remainder_limit_persistent (x z : T.Obj 0)
87     (hz : Tendsto (fun N => T.remainder N x) atTop (𝓝 z)) : z ∈ T.persistent := by
88   intro m
89   have h1 : Tendsto (fun N => T.remainder m (T.remainder N x)) atTop
90       (𝓝 (T.remainder m z)) := (T.remainder m).continuous.continuousAt.tendsto.comp hz
91   have h2 : Tendsto (fun N => T.remainder m (T.remainder N x)) atTop (𝓝 z) := by
92     apply hz.congr'
93     filter_upwards [eventually_ge_atTop m] with N hN
94     exact (T.remainder_nested_left m N hN x).symm
95   exact tendsto_nhds_unique h1 h2
96 
97 /-- A convergent remainder is an explicit boundary term in infinite reconstruction. -/
98 theorem reconstruction_with_boundary (x z : T.Obj 0)
99     (hz : Tendsto (fun N => T.remainder N x) atTop (𝓝 z)) :
100     Tendsto (fun N => ∑ n ∈ Finset.range N, T.detailTerm x n) atTop (𝓝 (x-z)) ∧
101     z ∈ T.persistent := by
102   constructor
103   · have hh := (tendsto_const_nhds (x := x)).sub hz
104     simpa only [← partial_apply, partial_eq_sum] using hh
105   · exact T.remainder_limit_persistent x z hz
106 
107 /-- Absolute summability yields a boundary term; it does not by itself kill it. -/
108 theorem absolutely_summable_boundary [CompleteSpace (T.Obj 0)] (x : T.Obj 0)
109     (hs : Summable (fun n => ‖T.detailTerm x n‖)) :
110     x - ∑' n, T.detailTerm x n ∈ T.persistent := by
111   have hsum := hs.of_norm.tendsto_sum_tsum_nat
112   have hz : Tendsto (fun N => T.remainder N x) atTop
113       (𝓝 (x - ∑' n, T.detailTerm x n)) := by
114     have hh := (tendsto_const_nhds (x := x)).sub hsum
115     simpa only [← partial_eq_sum, partial_apply, sub_sub_cancel] using hh
116   exact T.remainder_limit_persistent x _ hz
117 
118 /-- Absolute reconstruction is valid once the residual boundary is excluded. -/
119 theorem tsum_reconstruction [CompleteSpace (T.Obj 0)] (x : T.Obj 0)
120     (hs : Summable (fun n => ‖T.detailTerm x n‖))
121     (hp : T.persistent = ⊥) : (∑' n, T.detailTerm x n) = x := by
122   have h := T.absolutely_summable_boundary x hs
123   rw [hp, Submodule.mem_bot] at h
124   exact (sub_eq_zero.mp h).symm
125 
126 /-- Product gain for restoration, retaining possible amplification at each level. -/
127 def liftGain (N : ℕ) : ℝ := ∏ n ∈ Finset.range N, ‖(T.splitting n).lift‖
128 
129 @[simp] theorem liftGain_zero : T.liftGain 0 = 1 := by simp [liftGain]
130 @[simp] theorem liftGain_succ (N : ℕ) :
131     T.liftGain (N+1) = T.liftGain N * ‖(T.splitting N).lift‖ := by
132   simp [liftGain, Finset.prod_range_succ]
133 
134 theorem liftGain_nonneg (N : ℕ) : 0 ≤ T.liftGain N := by
135   unfold liftGain
136   exact Finset.prod_nonneg (fun n _ => norm_nonneg _)
137 
138 theorem restore_gain_bound (N : ℕ) (y : T.Obj N) :
139     ‖T.restore N y‖ ≤ T.liftGain N * ‖y‖ := by
140   induction N with
141   | zero => simp
142   | succ N ih =>
143     rw [restore_succ, liftGain_succ]
144     calc
145       _ ≤ T.liftGain N * ‖(T.splitting N).lift y‖ := ih _
146       _ ≤ T.liftGain N * (‖(T.splitting N).lift‖ * ‖y‖) :=
147         mul_le_mul_of_nonneg_left ((T.splitting N).lift.le_opNorm y) (T.liftGain_nonneg N)
148       _ = _ := (mul_assoc _ _ _).symm
149 
150 theorem reconstruction_error_bound (x : T.Obj 0) (N : ℕ) :
151     ‖x-T.reconstructed N x‖ ≤ T.liftGain N * ‖T.level x N‖ := by
152   rw [partial_error, remainder_apply]
153   exact T.restore_gain_bound _ _
154 
155 /-- Coarse decay after multiplication by the full restoration gain is sufficient. -/
156 theorem recoverable_of_weighted_coarse_decay (x : T.Obj 0)
157     (h : Tendsto (fun N => T.liftGain N * ‖T.level x N‖) atTop (𝓝 0)) :
158     x ∈ T.recoverable := by
159   apply tendsto_zero_iff_norm_tendsto_zero.mpr
160   apply squeeze_zero (fun _ => norm_nonneg _) _ h
161   intro N
162   rw [remainder_apply]
163   exact T.restore_gain_bound _ _
164 
165 /-- Quantitative geometric criterion allowing amplification and decay together. -/
166 theorem recoverable_of_geometric_bounds (x : T.Obj 0) (B C a b : ℝ)
167     (hB : 0 ≤ B) (_hC : 0 ≤ C) (ha : 0 ≤ a) (hb : 0 ≤ b)
168     (hgap : a*b < 1)
169     (hgain : ∀ N, T.liftGain N ≤ B*a^N)
170     (hcoarse : ∀ N, ‖T.level x N‖ ≤ C*b^N) :
171     x ∈ T.recoverable ∧
172     ∀ N, ‖x-T.reconstructed N x‖ ≤ (B*C)*(a*b)^N := by
173   have hbound (N : ℕ) : T.liftGain N * ‖T.level x N‖ ≤ (B*C)*(a*b)^N := by
174     calc
175       _ ≤ (B*a^N)*(C*b^N) := mul_le_mul (hgain N) (hcoarse N)
176         (norm_nonneg _) (mul_nonneg hB (pow_nonneg ha N))
177       _ = _ := by rw [mul_pow]; ring
178   constructor
179   · apply T.recoverable_of_weighted_coarse_decay
180     apply squeeze_zero (fun N => mul_nonneg (T.liftGain_nonneg N) (norm_nonneg _)) hbound
181     simpa only [mul_zero] using
182       (tendsto_pow_atTop_nhds_zero_of_lt_one (mul_nonneg ha hb) hgap).const_mul (B*C)
183   · intro N
184     exact (T.reconstruction_error_bound x N).trans (hbound N)
185 
186 /-- Contractive lifts cannot amplify the remaining coarse term. -/
187 theorem liftGain_le_one (hJ : ∀ n, ‖(T.splitting n).lift‖ ≤ 1) (N : ℕ) :
188     T.liftGain N ≤ 1 := by
189   induction N with
190   | zero => simp
191   | succ N ih =>
192     rw [liftGain_succ]
193     exact (mul_le_mul ih (hJ N) (norm_nonneg _) (by norm_num)).trans (by norm_num)
194 
195 theorem recoverable_of_coarse_decay (hJ : ∀ n, ‖(T.splitting n).lift‖ ≤ 1)
196     (x : T.Obj 0) (h : Tendsto (fun N => ‖T.level x N‖) atTop (𝓝 0)) :
197     x ∈ T.recoverable := by
198   apply T.recoverable_of_weighted_coarse_decay
199   apply squeeze_zero (fun N => mul_nonneg (T.liftGain_nonneg N) (norm_nonneg _)) _ h
200   intro N
201   simpa only [one_mul] using
202     mul_le_mul_of_nonneg_right (T.liftGain_le_one hJ N) (norm_nonneg (T.level x N))
203 
204 
205 end CoarseningCascade
206 end KomorebiSpace
207 end

Back to source controls