SequenceCascade.lean

1 import KomorebiSpace.CascadeDensity
2 import Mathlib.Analysis.Normed.Lp.lpSpace
3 import Mathlib.Tactic.NormNum
4 
5 set_option autoImplicit false
6 
7 /-!
8 # A concrete infinite cascade with exact reconstruction domain c₀
9 
10 This is a separate coordinate-shift coarsening model. It is not an assertion
11 that the transported dyadic maps equal shifts. All operators and norm bounds
12 are constructed on the actual space of bounded real sequences.
13 -/
14 noncomputable section
15 namespace KomorebiSpace
16 namespace SequenceCascade
17 open Filter
18 open scoped Topology ENNReal NNReal
19 
20 abbrev Space := lp (fun _ : ℕ => ℝ) (∞ : ℝ≥0∞)
21 
22 /-- Delete the first coordinate. -/
23 def tail (f : Space) : Space :=
24   ⟨fun k => f (k+1), memℓp_infty ⟨‖f‖, by
25     rintro _ ⟨k, rfl⟩
26     exact lp.norm_apply_le_norm ENNReal.top_ne_zero f (k+1)⟩⟩
27 
28 @[simp] theorem tail_apply (f : Space) (k : ℕ) : tail f k = f (k+1) := rfl
29 
30 theorem tail_bound (f : Space) : ‖tail f‖ ≤ ‖f‖ := by
31   apply lp.norm_le_of_forall_le (norm_nonneg f)
32   intro k
33   exact lp.norm_apply_le_norm ENNReal.top_ne_zero f (k+1)
34 
35 def downLinear : Space →ₗ[ℝ] Space where
36   toFun := tail
37   map_add' := by intros; apply lp.ext; rfl
38   map_smul' := by intros; apply lp.ext; rfl
39 
40 def down : Space →L[ℝ] Space := downLinear.mkContinuous 1 (fun f => by
41   change ‖tail f‖ ≤ 1*‖f‖
42   simpa only [one_mul] using tail_bound f)
43 
44 /-- Insert zero as the first coordinate. -/
45 def prepend (f : Space) : Space :=
46   ⟨(fun k => match k with | 0 => 0 | k+1 => f k), memℓp_infty ⟨‖f‖, by
47     rintro _ ⟨k, rfl⟩
48     cases k with
49     | zero => simpa only [norm_zero] using norm_nonneg f
50     | succ k => exact lp.norm_apply_le_norm ENNReal.top_ne_zero f k⟩⟩
51 
52 @[simp] theorem prepend_zero (f : Space) : prepend f 0 = 0 := rfl
53 @[simp] theorem prepend_succ (f : Space) (k : ℕ) : prepend f (k+1) = f k := rfl
54 
55 theorem prepend_bound (f : Space) : ‖prepend f‖ ≤ ‖f‖ := by
56   apply lp.norm_le_of_forall_le (norm_nonneg f)
57   intro k
58   cases k with
59   | zero => simpa only [prepend_zero, norm_zero] using norm_nonneg f
60   | succ k => exact lp.norm_apply_le_norm ENNReal.top_ne_zero f k
61 
62 def upLinear : Space →ₗ[ℝ] Space where
63   toFun := prepend
64   map_add' := by
65     intro f g
66     apply lp.ext
67     funext k
68     cases k <;> simp only [prepend_zero, prepend_succ, lp.coeFn_add, Pi.add_apply, add_zero]
69   map_smul' := by
70     intro c f
71     apply lp.ext
72     funext k
73     cases k <;> simp only [prepend_zero, prepend_succ, lp.coeFn_smul, Pi.smul_apply,
74       smul_zero, RingHom.id_apply]
75 
76 def up : Space →L[ℝ] Space := upLinear.mkContinuous 1 (fun f => by
77   change ‖prepend f‖ ≤ 1*‖f‖
78   simpa only [one_mul] using prepend_bound f)
79 
80 @[simp] theorem down_up (f : Space) : down (up f) = f := by
81   apply lp.ext
82   rfl
83 
84 /-- A single fully specified infinite coarsening cascade. -/
85 abbrev system : CoarseningCascade ℝ where
86   Obj _ := Space
87   down _ := down
88   splitting _ := { lift := up, right_inv := down_up }
89 
90 @[simp] theorem level_apply (f : Space) (N k : ℕ) :
91     system.level f N k = f (k+N) := by
92   induction N generalizing k with
93   | zero => rfl
94   | succ N ih =>
95     change system.level f N (k+1) = f (k+(N+1))
96     rw [ih, show k+1+N = k+(N+1) by omega]
97 
98 /-- The restored datum is padded by N leading zeros. -/
99 theorem restore_apply (f : Space) (N k : ℕ) :
100     system.restore N f k = if N ≤ k then f (k-N) else 0 := by
101   induction N generalizing f k with
102   | zero => change f k = if 0 ≤ k then f (k-0) else 0; simp
103   | succ N ih =>
104     change system.restore N (up f) k = _
105     rw [ih]
106     by_cases h : N+1 ≤ k
107     · have hNk : N ≤ k := by omega
108       have he : k-N = (k-(N+1))+1 := by omega
109       rw [ite_eq_left hNk, ite_eq_left h, he]
110       rfl
111     · rw [ite_eq_right h]
112       by_cases hNk : N ≤ k
113       · have he : k-N = 0 := by omega
114         rw [ite_eq_left hNk, he]
115         rfl
116       · rw [ite_eq_right hNk]
117 
118 /-- The original-space remainder is exactly the tail mask. -/
119 theorem remainder_apply (f : Space) (N k : ℕ) :
120     system.remainder N f k = if N ≤ k then f k else 0 := by
121   rw [CoarseningCascade.remainder_apply, restore_apply]
122   split_ifs with h
123   · rw [level_apply, Nat.sub_add_cancel h]
124   · rfl
125 
126 theorem remainder_bound (f : Space) (N : ℕ) : ‖system.remainder N f‖ ≤ ‖f‖ := by
127   apply lp.norm_le_of_forall_le (norm_nonneg f)
128   intro k
129   rw [remainder_apply]
130   split_ifs
131   · exact lp.norm_apply_le_norm ENNReal.top_ne_zero f k
132   · simpa only [norm_zero] using norm_nonneg f
133 
134 theorem remainder_opNorm (N : ℕ) : ‖system.remainder N‖ ≤ 1 := by
135   apply ContinuousLinearMap.opNorm_le_bound _ (by norm_num)
136   intro f
137   simpa only [one_mul] using remainder_bound f N
138 
139 /-- A concrete identification, not a declaration of a new convergence predicate. -/
140 theorem recoverable_iff_vanishes (f : Space) :
141     f ∈ system.recoverable ↔ Tendsto (fun n => f n) atTop (𝓝 0) := by
142   constructor
143   · intro h
144     apply tendsto_zero_iff_norm_tendsto_zero.mpr
145     apply squeeze_zero (fun _ => norm_nonneg _) _
146       (tendsto_zero_iff_norm_tendsto_zero.mp h)
147     intro N
148     have hh := lp.norm_apply_le_norm ENNReal.top_ne_zero (system.remainder N f) N
149     rw [remainder_apply f N N, ite_eq_left (le_refl N)] at hh
150     exact hh
151   · intro h
152     apply tendsto_zero_iff_norm_tendsto_zero.mpr
153     apply Metric.tendsto_atTop.mpr
154     intro ε hε
155     have hn := tendsto_zero_iff_norm_tendsto_zero.mp h
156     obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp hn (ε/2) (by positivity)
157     refine ⟨N, fun n hnN => ?_⟩
158     have hb : ‖system.remainder n f‖ ≤ ε/2 := by
159       apply lp.norm_le_of_forall_le (by positivity)
160       intro k
161       rw [remainder_apply]
162       split_ifs with hnk
163       · have hk := hN k (hnN.trans hnk)
164         have : ‖f k‖ < ε/2 := by
165           simpa only [Real.dist_eq, sub_zero, abs_of_nonneg (norm_nonneg _)] using hk
166         exact this.le
167       · simp only [norm_zero]; positivity
168     have hh : ‖system.remainder n f‖ < ε := by linarith
169     simpa only [Real.dist_eq, sub_zero, abs_of_nonneg (norm_nonneg _)] using hh
170 
171 /-- Explicit natural-order infinite reconstruction for every c₀ sequence. -/
172 theorem reconstruct_vanishing (f : Space)
173     (hf : Tendsto (fun n => f n) atTop (𝓝 0)) :
174     Tendsto (fun N => ∑ n ∈ Finset.range N, system.detailTerm f n) atTop (𝓝 f) := by
175   apply (system.ordered_reconstruction_iff f).2
176   exact (recoverable_iff_vanishes f).2 hf
177 
178 /-- No nonzero datum is invisible to every detail, even on the whole l-infinity space. -/
179 theorem persistent_eq_bot : system.persistent = ⊥ := by
180   apply le_antisymm _ bot_le
181   intro f hf
182   rw [Submodule.mem_bot]
183   apply lp.ext
184   funext k
185   have hh := congrArg (fun g : Space => g k) (hf (k+1))
186   rw [remainder_apply, ite_eq_right (by omega)] at hh
187   exact hh.symm
188 
189 /-- The constant-one sequence is bounded. -/
190 def ones : Space :=
191   ⟨fun _ => 1, memℓp_infty ⟨1, by rintro _ ⟨n, rfl⟩; norm_num⟩⟩
192 
193 /-- Its remainder never vanishes in norm despite the trivial persistent subspace. -/
194 theorem ones_remainder_norm (N : ℕ) : ‖system.remainder N ones‖ = 1 := by
195   apply le_antisymm
196   · apply lp.norm_le_of_forall_le (by norm_num)
197     intro k
198     rw [remainder_apply]
199     split_ifs <;> norm_num [ones]
200   · have hh := lp.norm_apply_le_norm ENNReal.top_ne_zero (system.remainder N ones) N
201     rw [remainder_apply ones N N, ite_eq_left (le_refl N)] at hh
202     simpa only [ones, norm_one] using hh
203 
204 theorem ones_not_recoverable : ones ∉ system.recoverable := by
205   intro h
206   have hh := tendsto_zero_iff_norm_tendsto_zero.mp h
207   have heq : (fun N => ‖system.remainder N ones‖) = (fun _ : ℕ => (1 : ℝ)) :=
208     funext ones_remainder_norm
209   rw [heq] at hh
210   have he : (1 : ℝ) = 0 := tendsto_nhds_unique tendsto_const_nhds hh
211   norm_num at he
212 
213 /-- Trivial persistent kernel and bounded remainders do not imply universal reconstruction. -/
214 theorem stability_and_separation_not_enough :
215     system.persistent = ⊥ ∧ (∀ N, ‖system.remainder N‖ ≤ 1) ∧
216     ∃ f : Space, f ∉ system.recoverable :=
217   ⟨persistent_eq_bot, remainder_opNorm, ones, ones_not_recoverable⟩
218 
219 /-- Each retained original-space detail is precisely a single coordinate. -/
220 theorem detailTerm_apply (f : Space) (n k : ℕ) :
221     system.detailTerm f n k = if k = n then f k else 0 := by
222   rw [CoarseningCascade.detailTerm_eq_remainder_sub]
223   change (system.remainder n f) k - (system.remainder (n+1) f) k = _
224   rw [remainder_apply, remainder_apply]
225   by_cases hkn : k = n
226   · subst k
227     simp
228   · by_cases hnk : n ≤ k
229     · have hsucc : n+1 ≤ k := by omega
230       simp [hnk, hsucc, hkn]
231     · have hsucc : ¬ n+1 ≤ k := by omega
232       simp [hnk, hsucc, hkn]
233 
234 /-- A nontrivial infinite family inside the recoverable domain. -/
235 def geometric (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) : Space :=
236   ⟨fun n => q^n, memℓp_infty ⟨1, by
237     rintro _ ⟨n, rfl⟩
238     change ‖q^n‖ ≤ 1
239     rw [Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hq0 n)]
240     exact pow_le_one₀ hq0 hq1.le⟩⟩
241 
242 @[simp] theorem geometric_apply (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) (n : ℕ) :
243     geometric q hq0 hq1 n = q^n := rfl
244 
245 theorem geometric_recoverable (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) :
246     geometric q hq0 hq1 ∈ system.recoverable := by
247   apply (recoverable_iff_vanishes _).2
248   exact tendsto_pow_atTop_nhds_zero_of_lt_one hq0 hq1
249 
250 /-- Exact error, not merely an upper estimate, at every truncation depth. -/
251 theorem geometric_remainder_norm (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) (N : ℕ) :
252     ‖system.remainder N (geometric q hq0 hq1)‖ = q^N := by
253   apply le_antisymm
254   · apply lp.norm_le_of_forall_le (pow_nonneg hq0 N)
255     intro k
256     rw [remainder_apply]
257     split_ifs with h
258     · rw [geometric_apply, Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hq0 k)]
259       obtain ⟨j, rfl⟩ := Nat.exists_eq_add_of_le h
260       rw [pow_add]
261       have hh : q^j ≤ 1 := pow_le_one₀ hq0 hq1.le
262       simpa only [mul_one] using mul_le_mul_of_nonneg_left hh (pow_nonneg hq0 N)
263     · simpa only [norm_zero] using pow_nonneg hq0 N
264   · have hh := lp.norm_apply_le_norm ENNReal.top_ne_zero
265       (system.remainder N (geometric q hq0 hq1)) N
266     rw [remainder_apply (geometric q hq0 hq1) N N, ite_eq_left (le_refl N),
267       geometric_apply, Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hq0 N)] at hh
268     exact hh
269 
270 theorem geometric_reconstruction_error (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) (N : ℕ) :
271     ‖geometric q hq0 hq1 - system.reconstructed N (geometric q hq0 hq1)‖ = q^N := by
272   exact (system.partial_error (geometric q hq0 hq1) N).trans
273     (geometric_remainder_norm q hq0 hq1 N)
274 
275 
276 end SequenceCascade
277 end KomorebiSpace
278 end

Back to source controls