CascadeProjections.lean

1 import KomorebiSpace.CoarseningCascade
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Nested remainder projections and persistent information
7 
8 All statements concern the actual coarsening/section cascade. The remainder
9 is restored to the original normed space before any limiting assertion.
10 The persistent subspace is not assumed trivial.
11 -/
12 universe u v
13 noncomputable section
14 namespace KomorebiSpace
15 namespace CoarseningCascade
16 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
17 variable (T : CoarseningCascade.{u,v} 𝕜)
18 
19 /-- Coarse observation, as a continuous linear operator. -/
20 def levelMap : ∀ n, T.Obj 0 →L[𝕜] T.Obj n
21   | 0 => ContinuousLinearMap.id 𝕜 (T.Obj 0)
22   | n+1 => (T.down n).comp (levelMap n)
23 
24 @[simp] theorem levelMap_apply (x : T.Obj 0) (n : ℕ) :
25     T.levelMap n x = T.level x n := by
26   induction n with
27   | zero => rfl
28   | succ n ih => change T.down n (T.levelMap n x) = _; rw [ih]; rfl
29 
30 /-- Lifted coarse remainder, expressed in the original candidate space. -/
31 def remainder (n : ℕ) : T.Obj 0 →L[𝕜] T.Obj 0 :=
32   (T.restore n).comp (T.levelMap n)
33 
34 @[simp] theorem remainder_apply (x : T.Obj 0) (n : ℕ) :
35     T.remainder n x = T.restore n (T.level x n) := by
36   simp only [remainder, ContinuousLinearMap.comp_apply, levelMap_apply]
37 
38 @[simp] theorem remainder_zero (x : T.Obj 0) : T.remainder 0 x = x := rfl
39 
40 /-- Every repeated section remains a right inverse at its own coarse level. -/
41 @[simp] theorem level_restore (n : ℕ) (y : T.Obj n) :
42     T.level (T.restore n y) n = y := by
43   induction n with
44   | zero => rfl
45   | succ n ih =>
46     rw [restore_succ, level_succ, ih]
47     exact (T.splitting n).right_inv y
48 
49 theorem restore_injective (n : ℕ) : Function.Injective (T.restore n) := by
50   intro x y h
51   have hh := congrArg (fun z => T.level z n) h
52   simpa only [level_restore] using hh
53 
54 @[simp] theorem remainder_restore (n : ℕ) (y : T.Obj n) :
55     T.remainder n (T.restore n y) = T.restore n y := by
56   rw [remainder_apply, level_restore]
57 
58 @[simp] theorem remainder_idempotent (n : ℕ) (x : T.Obj 0) :
59     T.remainder n (T.remainder n x) = T.remainder n x := by
60   simp only [remainder_apply, level_restore]
61 
62 /-- Restoring at level m leaves every coarser observation unchanged. -/
63 theorem level_remainder_of_le (m n : ℕ) (h : m ≤ n) (x : T.Obj 0) :
64     T.level (T.remainder m x) n = T.level x n := by
65   induction n, h using Nat.le_induction with
66   | base => rw [remainder_apply, level_restore]
67   | succ n h ih => rw [level_succ, ih, level_succ]
68 
69 /-- A finer remainder fixes every datum restored from a coarser level. -/
70 theorem remainder_restore_of_le (m n : ℕ) (h : m ≤ n) (y : T.Obj n) :
71     T.remainder m (T.restore n y) = T.restore n y := by
72   induction n, h using Nat.le_induction with
73   | base => exact T.remainder_restore m y
74   | succ n h ih =>
75     rw [restore_succ]
76     exact ih ((T.splitting n).lift y)
77 
78 /-- The projections are nested. -/
79 theorem remainder_nested_left (m n : ℕ) (h : m ≤ n) (x : T.Obj 0) :
80     T.remainder m (T.remainder n x) = T.remainder n x := by
81   rw [T.remainder_apply x n]
82   exact T.remainder_restore_of_le m n h _
83 
84 theorem remainder_nested_right (m n : ℕ) (h : m ≤ n) (x : T.Obj 0) :
85     T.remainder n (T.remainder m x) = T.remainder n x := by
86   rw [remainder_apply, T.level_remainder_of_le m n h, remainder_apply]
87 
88 /-- Unlike arbitrary repair projectors, these nested remainder projections commute. -/
89 theorem remainder_commute (m n : ℕ) (x : T.Obj 0) :
90     T.remainder m (T.remainder n x) = T.remainder n (T.remainder m x) := by
91   rcases le_total m n with h | h
92   · rw [T.remainder_nested_left m n h, T.remainder_nested_right m n h]
93   · rw [T.remainder_nested_right n m h, T.remainder_nested_left n m h]
94 
95 /-- A detail is the difference of two consecutive original-space remainders. -/
96 theorem detailTerm_eq_remainder_sub (x : T.Obj 0) (n : ℕ) :
97     T.detailTerm x n = T.remainder n x - T.remainder (n+1) x := by
98   have h := T.one_layer x n
99   rw [← remainder_apply, ← remainder_apply] at h
100   rw [h]
101   abel
102 
103 /-- The first N layers reconstructed in their natural order. -/
104 def reconstructed (N : ℕ) : T.Obj 0 →L[𝕜] T.Obj 0 :=
105   ContinuousLinearMap.id 𝕜 (T.Obj 0) - T.remainder N
106 
107 @[simp] theorem partial_apply (x : T.Obj 0) (N : ℕ) :
108     T.reconstructed N x = x - T.remainder N x := rfl
109 
110 theorem partial_eq_sum (x : T.Obj 0) (N : ℕ) :
111     T.reconstructed N x = ∑ n ∈ Finset.range N, T.detailTerm x n := by
112   have h := T.reconstruction x N
113   rw [← remainder_apply] at h
114   rw [partial_apply]
115   exact sub_eq_iff_eq_add.mpr h
116 
117 @[simp] theorem remainder_partial (x : T.Obj 0) (N : ℕ) :
118     T.remainder N (T.reconstructed N x) = 0 := by
119   rw [partial_apply, map_sub, remainder_idempotent, sub_self]
120 
121 @[simp] theorem partial_idempotent (x : T.Obj 0) (N : ℕ) :
122     T.reconstructed N (T.reconstructed N x) = T.reconstructed N x := by
123   rw [partial_apply, remainder_partial, sub_zero]
124 
125 /-- Persistent coarse information, invisible to every retained detail. -/
126 def persistent : Submodule 𝕜 (T.Obj 0) where
127   carrier := {x | ∀ n, T.remainder n x = x}
128   zero_mem' := by intro n; exact map_zero _
129   add_mem' := by intro x y hx hy n; rw [map_add, hx n, hy n]
130   smul_mem' := by intro c x hx n; rw [map_smul, hx n]
131 
132 @[simp] theorem mem_persistent (x : T.Obj 0) :
133     x ∈ T.persistent ↔ ∀ n, T.remainder n x = x := Iff.rfl
134 
135 /-- Vanishing all details alone is exactly membership in the persistent subspace. -/
136 theorem persistent_iff_details_zero (x : T.Obj 0) :
137     x ∈ T.persistent ↔ ∀ n, T.detail x n = 0 := by
138   constructor
139   · intro hx n
140     apply T.restore_injective n
141     change T.detailTerm x n = T.restore n 0
142     rw [map_zero, detailTerm_eq_remainder_sub, hx n, hx (n+1), sub_self]
143   · intro hx n
144     induction n with
145     | zero => rfl
146     | succ n ih =>
147       have hl := T.one_layer x n
148       have hd : T.detailTerm x n = 0 := by simp only [detailTerm, hx n, map_zero]
149       rw [← remainder_apply, ← remainder_apply, hd, zero_add] at hl
150       exact hl.symm.trans ih
151 
152 /-- Equal detail coordinates determine only a class modulo persistent information. -/
153 theorem equal_details_iff_persistent_difference (x y : T.Obj 0) :
154     (∀ n, T.detail x n = T.detail y n) ↔ x-y ∈ T.persistent := by
155   rw [persistent_iff_details_zero]
156   have hd (n : ℕ) : T.detail (x-y) n = T.detail x n - T.detail y n := by
157     unfold detail
158     rw [← levelMap_apply, map_sub, levelMap_apply, levelMap_apply, map_sub]
159   simp only [hd, sub_eq_zero]
160 
161 /-- The N-th coarse remainder has no retained detail below level N. -/
162 theorem remainder_details_below (x : T.Obj 0) (N j : ℕ) (hj : j < N) :
163     T.detail (T.remainder N x) j = 0 := by
164   apply T.restore_injective j
165   change T.detailTerm (T.remainder N x) j = T.restore j 0
166   rw [map_zero, detailTerm_eq_remainder_sub,
167     T.remainder_nested_left j N hj.le,
168     T.remainder_nested_left (j+1) N (by omega), sub_self]
169 
170 
171 end CoarseningCascade
172 end KomorebiSpace
173 end

Back to source controls