DyadicResidualSplit.lean

1 import KomorebiSpace.BoundedParity
2 import KomorebiSpace.ResidualSampling
3 import KomorebiSpace.SplitTowerCanonicity
4 
5 set_option autoImplicit false
6 
7 /-!
8 # A section of actual dyadic residual coarsening
9 
10 Target sections lift a coarse residual to the odd edge of each pair. The even
11 edge is zero. No source propagation-gap assumption is used.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace DyadicResidual
17 open BanachTower
18 open scoped NNReal ENNReal
19 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
20 variable (X Y : BanachTower.{u,v} 𝕜)
21 variable (hX : ∀ n, ‖X.down n‖ ≤ 1) (hY : ∀ n, ‖Y.down n‖ ≤ 1)
22 
23 abbrev schedule (n : ℕ) := 2*n
24 
25 theorem schedule_monotone : Monotone schedule := fun _ _ h => Nat.mul_le_mul_left 2 h
26 
27 theorem schedule_gap (n : ℕ) : schedule (n+1) - schedule n ≤ 2 := by
28   simp [schedule, Nat.mul_add]
29 
30 abbrev sampled (X : BanachTower.{u,v} 𝕜) (hX : ∀ n, ‖X.down n‖ ≤ 1) :=
31   resample X hX schedule schedule_monotone
32 
33 abbrev Coarse := Residuals (sampled X hX) (sampled Y hY)
34 
35 def coarsen : Residuals X Y →L[𝕜] Coarse X Y hX hY :=
36   residualSampleCLM X Y hX hY schedule schedule_monotone 2 schedule_gap
37 
38 /-- Coarse residuals are transported pair sums, not samples. -/
39 theorem coarsen_pair (r : Residuals X Y) (n : ℕ) :
40     coarsen X Y hX hY r n =
41       (Y.down (2*n)).comp (r (2*n+1)) + (r (2*n)).comp (X.down (2*n+1)) := by
42   change blockSum X Y r (show 2*n ≤ 2*(n+1) from schedule_monotone (Nat.le_succ n)) = _
43   rw [blockSum_succ X Y r (show 2*n ≤ 2*n+1 by omega)]
44   simp
45 
46 variable (L : Splitting Y)
47 
48 def oddLift (c : Coarse X Y hX hY) (n : ℕ) : X.Obj (2*n+1+1) →L[𝕜] Y.Obj (2*n+1) :=
49   (L.up (2*n)).comp (c n)
50 
51 theorem oddLift_bound (c : Coarse X Y hX hY) (n : ℕ) :
52     ‖oddLift X Y hX hY L c n‖ ≤ (L.bound : ℝ) * ‖c‖ := by
53   exact ((L.up (2*n)).opNorm_comp_le (c n)).trans
54     (mul_le_mul (L.up_bound _) (lp.norm_apply_le_norm ENNReal.top_ne_zero c n)
55       (norm_nonneg _) (NNReal.coe_nonneg _))
56 
57 def oddLiftFamily (c : Coarse X Y hX hY) :
58     BoundedParity.Odd (E := fun n => X.Obj (n+1) →L[𝕜] Y.Obj n) :=
59   ⟨oddLift X Y hX hY L c, memℓp_infty ⟨(L.bound : ℝ)*‖c‖, by
60     rintro _ ⟨n, rfl⟩
61     exact oddLift_bound X Y hX hY L c n⟩⟩
62 
63 def liftLinear : Coarse X Y hX hY →ₗ[𝕜] Residuals X Y where
64   toFun c := BoundedParity.merge (0, oddLiftFamily X Y hX hY L c)
65   map_add' c d := by
66     apply lp.ext
67     apply BoundedParity.family_ext
68     · intro n; simp only [BoundedParity.merge_even, lp.coeFn_add, Pi.add_apply]; simp
69     · intro n
70       simp only [BoundedParity.merge_odd, lp.coeFn_add, Pi.add_apply]
71       apply ContinuousLinearMap.ext
72       intro x
73       change L.up (2*n) (c n x + d n x) = L.up (2*n) (c n x) + L.up (2*n) (d n x)
74       exact map_add (L.up (2*n)) _ _
75   map_smul' a c := by
76     apply lp.ext
77     apply BoundedParity.family_ext
78     · intro n; simp only [BoundedParity.merge_even, lp.coeFn_smul, Pi.smul_apply]; simp
79     · intro n
80       simp only [BoundedParity.merge_odd, lp.coeFn_smul, Pi.smul_apply]
81       apply ContinuousLinearMap.ext
82       intro x
83       change L.up (2*n) (a • c n x) = a • L.up (2*n) (c n x)
84       exact map_smul (L.up (2*n)) a _
85 
86 theorem liftLinear_bound (c : Coarse X Y hX hY) :
87     ‖liftLinear X Y hX hY L c‖ ≤ (L.bound : ℝ) * ‖c‖ := by
88   apply (BoundedParity.merge_bound _).trans
89   change max ‖(0 : BoundedParity.Even (E := fun n => X.Obj (n+1) →L[𝕜] Y.Obj n))‖
90     ‖oddLiftFamily X Y hX hY L c‖ ≤ _
91   apply max_le
92   · simp only [norm_zero]; positivity
93   · apply lp.norm_le_of_forall_le (by positivity)
94     exact oddLift_bound X Y hX hY L c
95 
96 /-- A bounded right inverse for block coarsening, without a propagation gap. -/
97 def lift : Coarse X Y hX hY →L[𝕜] Residuals X Y :=
98   (liftLinear X Y hX hY L).mkContinuous (L.bound : ℝ) (liftLinear_bound X Y hX hY L)
99 
100 @[simp] theorem lift_even (c : Coarse X Y hX hY) (n : ℕ) :
101     lift X Y hX hY L c (2*n) = 0 := BoundedParity.merge_even _ n
102 
103 @[simp] theorem lift_odd (c : Coarse X Y hX hY) (n : ℕ) :
104     lift X Y hX hY L c (2*n+1) = (L.up (2*n)).comp (c n) :=
105   BoundedParity.merge_odd _ n
106 
107 theorem lift_bound (c : Coarse X Y hX hY) :
108     ‖lift X Y hX hY L c‖ ≤ (L.bound : ℝ)*‖c‖ := liftLinear_bound X Y hX hY L c
109 
110 theorem lift_opNorm : ‖lift X Y hX hY L‖ ≤ (L.bound : ℝ) :=
111   ContinuousLinearMap.opNorm_le_bound _ (NNReal.coe_nonneg _) (lift_bound X Y hX hY L)
112 
113 @[simp] theorem coarsen_lift (c : Coarse X Y hX hY) :
114     coarsen X Y hX hY (lift X Y hX hY L c) = c := by
115   apply lp.ext
116   funext n
117   rw [coarsen_pair, lift_even, lift_odd]
118   ext x
119   change Y.down (2*n) (L.up (2*n) (c n x)) + 0 = c n x
120   rw [L.down_up_apply, add_zero]
121 
122 /-- This is a section of the actual v0.6 block-accumulation operator. -/
123 def sectionC : SplitDefect.Section (coarsen X Y hX hY) where
124   lift := lift X Y hX hY L
125   right_inv := coarsen_lift X Y hX hY L
126 
127 /-- All residual information invisible to this choice of coarse observation. -/
128 def hidden : Residuals X Y →L[𝕜] Residuals X Y := (sectionC X Y hX hY L).project
129 
130 @[simp] theorem hidden_apply (r : Residuals X Y) :
131     hidden X Y hX hY L r = r - lift X Y hX hY L (coarsen X Y hX hY r) := rfl
132 
133 @[simp] theorem hidden_coarsen (r : Residuals X Y) :
134     coarsen X Y hX hY (hidden X Y hX hY L r) = 0 :=
135   (sectionC X Y hX hY L).project_exact r
136 
137 @[simp] theorem hidden_idempotent (r : Residuals X Y) :
138     hidden X Y hX hY L (hidden X Y hX hY L r) = hidden X Y hX hY L r :=
139   (sectionC X Y hX hY L).project_idempotent r
140 
141 @[simp] theorem hidden_even (r : Residuals X Y) (n : ℕ) :
142     hidden X Y hX hY L r (2*n) = r (2*n) := by simp [hidden_apply]
143 
144 @[simp] theorem hidden_odd (r : Residuals X Y) (n : ℕ) :
145     hidden X Y hX hY L r (2*n+1) =
146       r (2*n+1) - oddLift X Y hX hY L (coarsen X Y hX hY r) n := by
147   change (r - lift X Y hX hY L (coarsen X Y hX hY r)) (2*n+1) = _
148   change r (2*n+1) - lift X Y hX hY L (coarsen X Y hX hY r) (2*n+1) = _
149   rw [lift_odd]
150   rfl
151 
152 /-- Fine data are recovered exactly from coarse data and hidden detail. -/
153 theorem reconstruction (r : Residuals X Y) :
154     hidden X Y hX hY L r + lift X Y hX hY L (coarsen X Y hX hY r) = r := by
155   rw [hidden_apply]; abel
156 
157 /-- A complete characterization of the dyadic coarsening kernel. -/
158 theorem kernel_iff (r : Residuals X Y) : coarsen X Y hX hY r = 0 ↔
159     ∀ n, (Y.down (2*n)).comp (r (2*n+1)) = -(r (2*n)).comp (X.down (2*n+1)) := by
160   constructor
161   · intro h n
162     have hn := congrArg (fun c : Coarse X Y hX hY => c n) h
163     rw [coarsen_pair] at hn
164     exact eq_neg_of_add_eq_zero_left hn
165   · intro h
166     apply lp.ext
167     funext n
168     rw [coarsen_pair, h n]
169     ext x
170     change -(r (2*n) (X.down (2*n+1) x)) + r (2*n) (X.down (2*n+1) x) = 0
171     exact neg_add_cancel _
172 
173 /-- A continuous linear lossless residual coordinate system. -/
174 def coordinates : Residuals X Y ≃L[𝕜]
175     ((coarsen X Y hX hY).ker × Coarse X Y hX hY) := (sectionC X Y hX hY L).chart
176 
177 theorem reconstruction_bound (r : Residuals X Y) :
178     ‖r‖ ≤ ‖hidden X Y hX hY L r‖ + (L.bound : ℝ)*‖coarsen X Y hX hY r‖ := by
179   have hj := lift_bound X Y hX hY L (coarsen X Y hX hY r)
180   have ha := norm_add_le (hidden X Y hX hY L r)
181     (lift X Y hX hY L (coarsen X Y hX hY r))
182   rw [reconstruction] at ha
183   linarith only [ha, hj]
184 
185 theorem hidden_bound (r : Residuals X Y) :
186     ‖hidden X Y hX hY L r‖ ≤ (1 + 2*(L.bound : ℝ))*‖r‖ := by
187   have hj := lift_bound X Y hX hY L (coarsen X Y hX hY r)
188   have hc := residualSampleCLM_bound X Y hX hY schedule schedule_monotone 2 schedule_gap r
189   change ‖coarsen X Y hX hY r‖ ≤ 2*‖r‖ at hc
190   have hm := mul_le_mul_of_nonneg_left hc (NNReal.coe_nonneg L.bound)
191   have ha := norm_sub_le r (lift X Y hX hY L (coarsen X Y hX hY r))
192   rw [hidden_apply]
193   nlinarith only [ha, hj, hm]
194 
195 /-- Coarse exactness plus zero retained detail is equivalent to fine exactness. -/
196 theorem exactness_detected (f : Candidates X Y) :
197     Exact X Y f ↔
198       Exact (sampled X hX) (sampled Y hY)
199         (sampleCLM X Y hX hY schedule schedule_monotone f) ∧
200       hidden X Y hX hY L (differential X Y f) = 0 := by
201   rw [exact_iff_differential_zero, exact_iff_differential_zero,
202     resampling_chain X Y hX hY schedule schedule_monotone 2 schedule_gap]
203   constructor
204   · intro h
205     simp [h]
206   · rintro ⟨hc, hh⟩
207     change coarsen X Y hX hY (differential X Y f) = 0 at hc
208     have h := reconstruction X Y hX hY L (differential X Y f)
209     rw [hc, hh, map_zero, zero_add] at h
210     exact h.symm
211 
212 end DyadicResidual
213 end KomorebiSpace
214 end

Back to source controls