CascadeBoundaryExamples.lean

1 import KomorebiSpace.CascadeLimits
2 import Mathlib.Tactic.NormNum
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Coarse decay and detail summability do not remove the persistent term
8 
9 A completely specified scalar cascade has down=1/2 and lift=2. Its coarse
10 coordinates tend to zero, but restoring them gives back the entire input.
11 -/
12 noncomputable section
13 namespace KomorebiSpace
14 namespace CascadeBoundaryExamples
15 open Filter
16 open scoped Topology
17 
18 abbrev scalarDown : ℝ →L[ℝ] ℝ := (1/2 : ℝ) • ContinuousLinearMap.id ℝ ℝ
19 abbrev scalarUp : ℝ →L[ℝ] ℝ := (2 : ℝ) • ContinuousLinearMap.id ℝ ℝ
20 
21 theorem scalar_right_inv (x : ℝ) : scalarDown (scalarUp x) = x := by
22   change (1/2 : ℝ)*(2*x)=x
23   ring
24 
25 abbrev system : CoarseningCascade ℝ where
26   Obj _ := ℝ
27   down _ := scalarDown
28   splitting _ := { lift := scalarUp, right_inv := scalar_right_inv }
29 
30 @[simp] theorem level_formula (x : ℝ) (N : ℕ) :
31     system.level x N = (1/2 : ℝ)^N*x := by
32   induction N with
33   | zero => simp
34   | succ N ih =>
35     change (1/2 : ℝ)*system.level x N = _
36     rw [ih, pow_succ]
37     ring
38 
39 @[simp] theorem restore_formula (x : ℝ) (N : ℕ) :
40     system.restore N x = (2 : ℝ)^N*x := by
41   induction N generalizing x with
42   | zero => change x = (2 : ℝ)^0*x; simp
43   | succ N ih =>
44     change system.restore N (2*x) = _
45     rw [ih, pow_succ]
46     ring
47 
48 @[simp] theorem remainder_identity (x : ℝ) (N : ℕ) : system.remainder N x = x := by
49   rw [CoarseningCascade.remainder_apply, level_formula, restore_formula]
50   rw [← mul_assoc, ← mul_pow]
51   norm_num
52 
53 @[simp] theorem every_detail_zero (x : ℝ) (N : ℕ) : system.detail x N = 0 := by
54   exact (system.persistent_iff_details_zero x).1 (fun n => remainder_identity x n) N
55 
56 @[simp] theorem every_detailTerm_zero (x : ℝ) (N : ℕ) : system.detailTerm x N = 0 := by
57   simp only [CoarseningCascade.detailTerm, every_detail_zero, map_zero]
58 
59 /-- Every coarse coordinate tends to zero, including those of nonzero inputs. -/
60 theorem coarse_tends_zero (x : ℝ) :
61     Tendsto (fun N => system.level x N) atTop (𝓝 0) := by
62   have h := (tendsto_pow_atTop_nhds_zero_of_lt_one
63     (show (0 : ℝ) ≤ 1/2 by norm_num) (show (1/2 : ℝ) < 1 by norm_num)).mul_const x
64   simpa only [level_formula, zero_mul] using h
65 
66 /-- Vanishing coarse coordinates plus summable details does not imply recovery. -/
67 theorem coarse_decay_and_summability_not_enough :
68     Tendsto (fun N => system.level (1 : ℝ) N) atTop (𝓝 0) ∧
69     Summable (fun N => ‖system.detailTerm (1 : ℝ) N‖) ∧
70     (1 : ℝ) ∉ system.recoverable := by
71   refine ⟨coarse_tends_zero 1, ?_, ?_⟩
72   · simp only [every_detailTerm_zero, norm_zero]
73     exact summable_zero
74   · intro h
75     change Tendsto (fun N => system.remainder N (1 : ℝ)) atTop (𝓝 0) at h
76     have hh : Tendsto (fun _ : ℕ => (1 : ℝ)) atTop (𝓝 0) := by
77       have heq : (fun N => system.remainder N (1 : ℝ)) = (fun _ : ℕ => (1 : ℝ)) :=
78         funext (remainder_identity 1)
79       rw [heq] at h
80       exact h
81     have he : (1 : ℝ) = 0 := tendsto_nhds_unique tendsto_const_nhds hh
82     norm_num at he
83 
84 end CascadeBoundaryExamples
85 end KomorebiSpace
86 end

Back to source controls