DyadicInfiniteReconstruction.lean

1 import KomorebiSpace.DyadicResidualHierarchy
2 import KomorebiSpace.CascadeDensity
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Infinite retained-detail reconstruction for the actual dyadic tower residual
8 
9 All-level detail injectivity is proved from the actual parity lift, without a
10 convergence assumption. Norm reconstruction requires a separate analytic
11 condition. No arbitrary replacement of the tower coarsening by a scalar model
12 is used in these theorems.
13 -/
14 universe u v
15 noncomputable section
16 namespace KomorebiSpace
17 namespace DyadicResidual
18 namespace System
19 open BanachTower Filter
20 open scoped Topology
21 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
22 variable (T : System.{u,v} 𝕜)
23 
24 /-- An explicitly typed view of the actual residual at coarsening depth j. -/
25 def residualLevel (r : Residuals T.source T.target) (j : ℕ) :
26     Residuals (T.stage j).source (T.stage j).target := T.cascade.level r j
27 
28 /-- All details determine every fine coordinate, via strong induction on its index. -/
29 theorem all_details_zero_implies_zero (r : Residuals T.source T.target)
30     (hd : ∀ j, T.cascade.detail r j = 0) : r = 0 := by
31   have hcoord : ∀ k j, T.residualLevel r j k = 0 := by
32     intro k
33     induction k using Nat.strong_induction_on with
34     | h k ih =>
35       intro j
36       let U := T.stage j
37       have hh : hidden U.source U.target U.source_contractive U.target_contractive
38           U.target_splitting (T.residualLevel r j) = 0 := hd j
39       have hpar : k = 2*(k/2) ∨ k = 2*(k/2)+1 := by omega
40       rcases hpar with he | ho
41       · have hv := congrArg (fun f : Residuals U.source U.target => f (2*(k/2))) hh
42         rw [hidden_even] at hv
43         rw [he]
44         exact hv
45       · have hv := congrArg (fun f : Residuals U.source U.target => f (2*(k/2)+1)) hh
46         rw [hidden_odd] at hv
47         have hk : k/2 < k := by omega
48         have hc : coarsen U.source U.target U.source_contractive U.target_contractive
49             (T.residualLevel r j) (k/2) = 0 := ih (k/2) hk (j+1)
50         change T.residualLevel r j (2*(k/2)+1) -
51           (U.target_splitting.up (2*(k/2))).comp
52             (coarsen U.source U.target U.source_contractive U.target_contractive
53               (T.residualLevel r j) (k/2)) = 0 at hv
54         rw [hc, ContinuousLinearMap.comp_zero, sub_zero] at hv
55         rw [ho]
56         exact hv
57   apply lp.ext
58   funext k
59   exact hcoord k 0
60 
61 /-- Unlike arbitrary split cascades, this actual dyadic cascade has no invisible
62 nonzero persistent residual. -/
63 theorem persistent_residual_eq_bot : T.cascade.persistent = ⊥ := by
64   apply le_antisymm _ bot_le
65   intro r hr
66   rw [Submodule.mem_bot]
67   exact T.all_details_zero_implies_zero r
68     ((T.cascade.persistent_iff_details_zero r).1 hr)
69 
70 /-- All detail coordinates are lossless at infinite depth, without norm convergence. -/
71 theorem infinite_details_injective (r s : Residuals T.source T.target)
72     (h : ∀ j, T.cascade.detail r j = T.cascade.detail s j) : r = s := by
73   have hm := (T.cascade.equal_details_iff_persistent_difference r s).1 h
74   rw [T.persistent_residual_eq_bot, Submodule.mem_bot] at hm
75   exact sub_eq_zero.mp hm
76 
77 /-- Every-scale detail vanishing detects actual fine compatibility. -/
78 theorem exactness_iff_all_details (f : Candidates T.source T.target) :
79     Exact T.source T.target f ↔
80     ∀ j, T.cascade.detail (differential T.source T.target f) j = 0 := by
81   rw [exact_iff_differential_zero]
82   constructor
83   · intro h j; rw [h]; exact T.cascade.detail_zero j
84   · exact T.all_details_zero_implies_zero _
85 
86 /-- Norm reconstruction has its own, strictly analytic, criterion. -/
87 theorem ordered_residual_reconstruction_iff (r : Residuals T.source T.target) :
88     Tendsto (fun N => ∑ n ∈ Finset.range N, T.cascade.detailTerm r n) atTop (𝓝 r) ↔
89     Tendsto (fun N => T.cascade.remainder N r) atTop (𝓝 0) :=
90   T.cascade.ordered_reconstruction_iff r
91 
92 theorem cascade_zero_complete : CompleteSpace (T.cascade.Obj 0) := by
93   change CompleteSpace (Residuals T.source T.target)
94   infer_instance
95 
96 /-- Absolute summability is now enough because the dyadic persistent space was
97 proved trivial, rather than assumed so. -/
98 theorem absolute_residual_reconstruction (r : Residuals T.source T.target)
99     (hs : Summable (fun n => ‖T.cascade.detailTerm r n‖)) :
100     (∑' n, T.cascade.detailTerm r n) = r := by
101   let : CompleteSpace (T.cascade.Obj 0) := T.cascade_zero_complete
102   exact T.cascade.tsum_reconstruction r hs T.persistent_residual_eq_bot
103 
104 /-- Any convergent dyadic remainder must converge to zero. -/
105 theorem convergent_remainder_zero (r z : Residuals T.source T.target)
106     (hz : Tendsto (fun N => T.cascade.remainder N r) atTop (𝓝 z)) : z = 0 := by
107   have hp := T.cascade.remainder_limit_persistent r z hz
108   rw [T.persistent_residual_eq_bot] at hp
109   change z = 0 at hp
110   exact hp
111 
112 /-- The section bound stays at most one under actual dyadic composition. -/
113 theorem stage_section_bound_le_one (hL : T.target_splitting.bound ≤ 1) (n : ℕ) :
114     (T.stage n).target_splitting.bound ≤ 1 := by
115   induction n with
116   | zero => exact hL
117   | succ n ih =>
118     change (T.stage n).target_splitting.bound * (T.stage n).target_splitting.bound ≤ 1
119     exact (mul_le_mul ih ih (by positivity) (by positivity)).trans (by norm_num)
120 
121 theorem cascade_lifts_contractive (hL : T.target_splitting.bound ≤ 1) (n : ℕ) :
122     ‖(T.cascade.splitting n).lift‖ ≤ 1 := by
123   let U := T.stage n
124   change ‖lift U.source U.target U.source_contractive U.target_contractive U.target_splitting‖ ≤ 1
125   exact (lift_opNorm U.source U.target U.source_contractive U.target_contractive
126     U.target_splitting).trans (by exact_mod_cast T.stage_section_bound_le_one hL n)
127 
128 /-- When section norms are at most one, no amplification factor is required. -/
129 theorem residual_reconstruction_of_coarse_decay (hL : T.target_splitting.bound ≤ 1)
130     (r : Residuals T.source T.target)
131     (hr : Tendsto (fun N => ‖T.cascade.level r N‖) atTop (𝓝 0)) :
132     Tendsto (fun N => ∑ n ∈ Finset.range N, T.cascade.detailTerm r n) atTop (𝓝 r) := by
133   apply (T.cascade.ordered_reconstruction_iff r).2
134   exact T.cascade.recoverable_of_coarse_decay (T.cascade_lifts_contractive hL) r hr
135 
136 /-- Typed finite reconstruction on the original residual space. -/
137 def reconstructedResidual (N : ℕ) :
138     Residuals T.source T.target →L[𝕜] Residuals T.source T.target :=
139   T.cascade.reconstructed N
140 
141 /-- Finite error estimate in the same contractive-section case. -/
142 theorem residual_error_le_coarse (hL : T.target_splitting.bound ≤ 1)
143     (r : Residuals T.source T.target) (N : ℕ) :
144     ‖r - T.reconstructedResidual N r‖ ≤ ‖T.cascade.level r N‖ := by
145   apply (T.cascade.reconstruction_error_bound r N).trans
146   simpa only [one_mul] using mul_le_mul_of_nonneg_right
147     (T.cascade.liftGain_le_one (T.cascade_lifts_contractive hL) N) (norm_nonneg _)
148 
149 /-- Vanishing N successive details determines the first 2^N-1 coordinates
150 at the starting scale. The target/source operator fibers remain the actual ones. -/
151 theorem finite_details_zero_coordinate (r : Residuals T.source T.target)
152     (N j k : ℕ)
153     (hd : ∀ i < N, T.cascade.detail r (j+i) = 0)
154     (hk : k+1 < 2^N) : T.residualLevel r j k = 0 := by
155   induction N generalizing j k with
156   | zero => simp only [pow_zero] at hk; omega
157   | succ N ih =>
158     let U := T.stage j
159     have hh : hidden U.source U.target U.source_contractive U.target_contractive
160         U.target_splitting (T.residualLevel r j) = 0 := by
161       have h := hd 0 (Nat.zero_lt_succ N)
162       rw [Nat.add_zero] at h
163       exact h
164     have hpar : k = 2*(k/2) ∨ k = 2*(k/2)+1 := by omega
165     rcases hpar with he | ho
166     · have hv := congrArg (fun f : Residuals U.source U.target => f (2*(k/2))) hh
167       rw [hidden_even] at hv
168       rw [he]
169       exact hv
170     · have hv := congrArg (fun f : Residuals U.source U.target => f (2*(k/2)+1)) hh
171       rw [hidden_odd] at hv
172       have hk' : k/2+1 < 2^N := by rw [pow_succ] at hk; omega
173       have hd' : ∀ i < N, T.cascade.detail r ((j+1)+i) = 0 := by
174         intro i hi
175         rw [show j+1+i = j+(i+1) by omega]
176         exact hd (i+1) (by omega)
177       have hc : coarsen U.source U.target U.source_contractive U.target_contractive
178           (T.residualLevel r j) (k/2) = 0 := ih (j+1) (k/2) hd' hk'
179       change T.residualLevel r j (2*(k/2)+1) -
180         (U.target_splitting.up (2*(k/2))).comp
181           (coarsen U.source U.target U.source_contractive U.target_contractive
182             (T.residualLevel r j) (k/2)) = 0 at hv
183       rw [hc, ContinuousLinearMap.comp_zero, sub_zero] at hv
184       rw [ho]
185       exact hv
186 
187 /-- An explicitly typed original-space remainder. -/
188 def residualRemainder (N : ℕ) :
189     Residuals T.source T.target →L[𝕜] Residuals T.source T.target := T.cascade.remainder N
190 
191 /-- Restored dyadic remainders are supported beyond the first 2^N-1 coordinates. -/
192 theorem remainder_coordinate_zero (r : Residuals T.source T.target) (N k : ℕ)
193     (hk : k+1 < 2^N) : T.residualRemainder N r k = 0 := by
194   have hd : ∀ i < N, T.cascade.detail (T.residualRemainder N r) (0+i) = 0 := by
195     intro i hi
196     rw [Nat.zero_add]
197     exact T.cascade.remainder_details_below r N i hi
198   exact T.finite_details_zero_coordinate (T.residualRemainder N r) N 0 k hd hk
199 
200 /-- Every fixed coordinate is reconstructed exactly after a finite depth. -/
201 theorem reconstruction_coordinate (r : Residuals T.source T.target) (N k : ℕ)
202     (hk : k+1 < 2^N) : T.reconstructedResidual N r k = r k := by
203   change r k - T.residualRemainder N r k = r k
204   rw [T.remainder_coordinate_zero r N k hk, sub_zero]
205 
206 /-- Coordinatewise operator-norm reconstruction holds for every bounded residual,
207 even when reconstruction in the uniform residual norm fails. -/
208 theorem coordinatewise_reconstruction (r : Residuals T.source T.target) (k : ℕ) :
209     Tendsto (fun N => T.reconstructedResidual N r k) atTop (𝓝 (r k)) := by
210   apply tendsto_const_nhds.congr'
211   filter_upwards [eventually_ge_atTop (k+1)] with N hN
212   exact (T.reconstruction_coordinate r N k (hN.trans_lt N.lt_two_pow_self)).symm
213 
214 
215 end System
216 end DyadicResidual
217 end KomorebiSpace
218 end

Back to source controls