CoarseningCascade.lean

1 import KomorebiSpace.SplitDefectCharts
2 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Finite, lossless hierarchies of split coarsenings
8 
9 Every discarded layer is retained in the kernel of its own coarsening map.
10 The reconstruction is finite and exact. No infinite-series convergence,
11 uniform multiscale bound, or computational compression is asserted.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 
17 structure CoarseningCascade (𝕜 : Type u) [NontriviallyNormedField 𝕜] where
18   Obj : ℕ → Type v
19   [normed : ∀ n, NormedAddCommGroup (Obj n)]
20   [space : ∀ n, NormedSpace 𝕜 (Obj n)]
21   down : ∀ n, Obj n →L[𝕜] Obj (n+1)
22   splitting : ∀ n, SplitDefect.Section (down n)
23 
24 attribute [instance] CoarseningCascade.normed CoarseningCascade.space
25 
26 namespace CoarseningCascade
27 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
28 variable (T : CoarseningCascade.{u,v} 𝕜)
29 
30 /-- Repeated coarse observation, with the original datum at level zero. -/
31 def level (x : T.Obj 0) : ∀ n, T.Obj n
32   | 0 => x
33   | n+1 => T.down n (level x n)
34 
35 /-- Lift a coarse datum back to the original space using the selected sections. -/
36 def restore : ∀ n, T.Obj n →L[𝕜] T.Obj 0
37   | 0 => ContinuousLinearMap.id 𝕜 (T.Obj 0)
38   | n+1 => (restore n).comp (T.splitting n).lift
39 
40 @[simp] theorem level_zero (x : T.Obj 0) : T.level x 0 = x := rfl
41 @[simp] theorem level_succ (x : T.Obj 0) (n : ℕ) :
42     T.level x (n+1) = T.down n (T.level x n) := rfl
43 @[simp] theorem restore_zero (x : T.Obj 0) : T.restore 0 x = x := rfl
44 @[simp] theorem restore_succ (n : ℕ) (y : T.Obj (n+1)) :
45     T.restore (n+1) y = T.restore n ((T.splitting n).lift y) := rfl
46 
47 @[simp] theorem level_of_zero (n : ℕ) : T.level 0 n = 0 := by
48   induction n with
49   | zero => rfl
50   | succ n ih => rw [level_succ, ih, map_zero]
51 
52 /-- The hidden residual at its own scale. -/
53 def detail (x : T.Obj 0) (n : ℕ) : T.Obj n :=
54   (T.splitting n).project (T.level x n)
55 
56 @[simp] theorem detail_hidden (x : T.Obj 0) (n : ℕ) : T.down n (T.detail x n) = 0 :=
57   (T.splitting n).project_exact _
58 
59 @[simp] theorem detail_zero (n : ℕ) : T.detail 0 n = 0 := by
60   unfold detail
61   rw [level_of_zero, map_zero]
62 
63 /-- The same detail transported into the original space. -/
64 def detailTerm (x : T.Obj 0) (n : ℕ) : T.Obj 0 := T.restore n (T.detail x n)
65 
66 theorem one_layer (x : T.Obj 0) (n : ℕ) :
67     T.restore n (T.level x n) = T.detailTerm x n + T.restore (n+1) (T.level x (n+1)) := by
68   unfold detailTerm detail
69   rw [SplitDefect.Section.project_apply, map_sub, restore_succ, level_succ]
70   abel
71 
72 /-- Exact finite multiscale reconstruction, for every depth N. -/
73 theorem reconstruction (x : T.Obj 0) (N : ℕ) :
74     x = (∑ n ∈ Finset.range N, T.detailTerm x n) + T.restore N (T.level x N) := by
75   induction N with
76   | zero => simp
77   | succ N ih =>
78     calc
79       x = (∑ n ∈ Finset.range N, T.detailTerm x n) + T.restore N (T.level x N) := ih
80       _ = (∑ n ∈ Finset.range N, T.detailTerm x n) +
81           (T.detailTerm x N + T.restore (N+1) (T.level x (N+1))) := by rw [one_layer]
82       _ = _ := by rw [Finset.sum_range_succ]; abel
83 
84 /-- The entire retained hierarchy detects equality, including the depth-zero case. -/
85 theorem equal_iff (x y : T.Obj 0) (N : ℕ) : x = y ↔
86     (∀ n < N, T.detail x n = T.detail y n) ∧ T.level x N = T.level y N := by
87   constructor
88   · rintro rfl; exact ⟨fun _ _ => rfl, rfl⟩
89   · rintro ⟨hd, hc⟩
90     have hs : (∑ n ∈ Finset.range N, T.detailTerm x n) =
91         ∑ n ∈ Finset.range N, T.detailTerm y n := by
92       apply Finset.sum_congr rfl
93       intro n hn
94       unfold detailTerm
95       rw [hd n (Finset.mem_range.mp hn)]
96     calc
97       x = (∑ n ∈ Finset.range N, T.detailTerm x n) + T.restore N (T.level x N) := T.reconstruction x N
98       _ = (∑ n ∈ Finset.range N, T.detailTerm y n) + T.restore N (T.level y N) := by rw [hs, hc]
99       _ = y := (T.reconstruction y N).symm
100 
101 theorem zero_iff (x : T.Obj 0) (N : ℕ) : x = 0 ↔
102     (∀ n < N, T.detail x n = 0) ∧ T.level x N = 0 := by
103   simpa only [detail_zero, level_of_zero] using T.equal_iff x 0 N
104 
105 end CoarseningCascade
106 end KomorebiSpace
107 end

Back to source controls