DyadicResidualDetails.lean

1 import KomorebiSpace.DyadicResidualSplit
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Explicit hidden-detail channels
7 
8 Within each pair, retain the even residual and the component of the odd
9 residual killed by target restriction. Together with the coarse residual,
10 these channels admit exact reconstruction. Every bounded independent choice
11 of the channels, with the stated kernel constraint, is realized uniquely.
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 variable (L : Splitting Y)
23 
24 abbrev EvenResidual := BoundedParity.Even (E := fun n => X.Obj (n+1) →L[𝕜] Y.Obj n)
25 abbrev OddResidual := BoundedParity.Odd (E := fun n => X.Obj (n+1) →L[𝕜] Y.Obj n)
26 
27 /-- The odd residual component invisible under target restriction. -/
28 def innovation (r : Residuals X Y) (n : ℕ) : X.Obj (2*n+1+1) →L[𝕜] Y.Obj (2*n+1) :=
29   r (2*n+1) - (L.up (2*n)).comp ((Y.down (2*n)).comp (r (2*n+1)))
30 
31 @[simp] theorem innovation_down (r : Residuals X Y) (n : ℕ) :
32     (Y.down (2*n)).comp (innovation X Y L r n) = 0 := by
33   ext x
34   change Y.down (2*n) (r (2*n+1) x - L.up (2*n) (Y.down (2*n) (r (2*n+1) x))) = 0
35   rw [map_sub, L.down_up_apply, sub_self]
36 
37 theorem innovation_add (r t : Residuals X Y) (n : ℕ) :
38     innovation X Y L (r+t) n = innovation X Y L r n + innovation X Y L t n := by
39   ext x
40   simp only [innovation, lp.coeFn_add, Pi.add_apply, ContinuousLinearMap.comp_apply,
41     sub_apply, add_apply, map_add]
42   abel
43 
44 theorem innovation_sub (r t : Residuals X Y) (n : ℕ) :
45     innovation X Y L (r-t) n = innovation X Y L r n - innovation X Y L t n := by
46   ext x
47   simp only [innovation, lp.coeFn_sub, Pi.sub_apply, ContinuousLinearMap.comp_apply,
48     sub_apply, map_sub]
49   abel
50 
51 @[simp] theorem innovation_zero (n : ℕ) : innovation X Y L 0 n = 0 := by
52   ext x
53   change 0 - L.up (2*n) (Y.down (2*n) 0) = 0
54   simp
55 
56 @[simp] theorem innovation_lift (c : Coarse X Y hX hY) (n : ℕ) :
57     innovation X Y L (lift X Y hX hY L c) n = 0 := by
58   unfold innovation
59   rw [lift_odd]
60   ext x
61   change L.up (2*n) (c n x) - L.up (2*n) (Y.down (2*n) (L.up (2*n) (c n x))) = 0
62   rw [L.down_up_apply, sub_self]
63 
64 @[simp] theorem innovation_hidden (r : Residuals X Y) (n : ℕ) :
65     innovation X Y L (hidden X Y hX hY L r) n = innovation X Y L r n := by
66   rw [hidden_apply, innovation_sub, innovation_lift, sub_zero]
67 
68 theorem innovation_smul (a : 𝕜) (r : Residuals X Y) (n : ℕ) :
69     innovation X Y L (a • r) n = a • innovation X Y L r n := by
70   ext x
71   simp only [innovation, lp.coeFn_smul, Pi.smul_apply, ContinuousLinearMap.comp_apply,
72     sub_apply, smul_apply, map_smul, smul_sub]
73 
74 include hY in
75 theorem innovation_bound (r : Residuals X Y) (n : ℕ) :
76     ‖innovation X Y L r n‖ ≤ (1+(L.bound : ℝ))*‖r‖ := by
77   have hb := lp.norm_apply_le_norm ENNReal.top_ne_zero r (2*n+1)
78   have hv : ‖(Y.down (2*n)).comp (r (2*n+1))‖ ≤ ‖r (2*n+1)‖ :=
79     ((Y.down (2*n)).opNorm_comp_le _).trans
80       (by simpa only [one_mul] using mul_le_mul_of_nonneg_right (hY (2*n)) (norm_nonneg (r (2*n+1))))
81   have hj : ‖(L.up (2*n)).comp ((Y.down (2*n)).comp (r (2*n+1)))‖ ≤
82       (L.bound : ℝ)*‖r (2*n+1)‖ :=
83     ((L.up (2*n)).opNorm_comp_le _).trans
84       (mul_le_mul (L.up_bound _) hv (norm_nonneg _) (NNReal.coe_nonneg _))
85   have hm := mul_le_mul_of_nonneg_left hb (NNReal.coe_nonneg L.bound)
86   have ha := norm_sub_le (r (2*n+1)) ((L.up (2*n)).comp ((Y.down (2*n)).comp (r (2*n+1))))
87   change ‖innovation X Y L r n‖ ≤ _ at ha
88   nlinarith only [hb, hj, hm, ha]
89 
90 def innovationFamily (r : Residuals X Y) : OddResidual X Y :=
91   ⟨innovation X Y L r, memℓp_infty ⟨(1+(L.bound : ℝ))*‖r‖, by
92     rintro _ ⟨n, rfl⟩
93     exact innovation_bound X Y hY L r n⟩⟩
94 
95 theorem innovationFamily_bound (r : Residuals X Y) :
96     ‖innovationFamily X Y hY L r‖ ≤ (1+(L.bound : ℝ))*‖r‖ := by
97   apply lp.norm_le_of_forall_le (by positivity)
98   exact innovation_bound X Y hY L r
99 
100 
101 /-- Reconstruction at a single odd edge, retaining both sorts of hidden detail. -/
102 theorem reconstruct_odd (r : Residuals X Y) (n : ℕ) :
103     r (2*n+1) = innovation X Y L r n + (L.up (2*n)).comp
104       (coarsen X Y hX hY r n - (r (2*n)).comp (X.down (2*n+1))) := by
105   rw [coarsen_pair, add_sub_cancel_right]
106   unfold innovation
107   abel
108 
109 theorem hidden_odd_details (r : Residuals X Y) (n : ℕ) :
110     hidden X Y hX hY L r (2*n+1) = innovation X Y L r n -
111       (L.up (2*n)).comp ((r (2*n)).comp (X.down (2*n+1))) := by
112   rw [hidden_odd]
113   unfold oddLift innovation
114   rw [coarsen_pair, ContinuousLinearMap.comp_add]
115   abel
116 
117 /-- The three channels jointly distinguish every bounded residual family. -/
118 theorem channels_injective (r t : Residuals X Y)
119     (hc : coarsen X Y hX hY r = coarsen X Y hX hY t)
120     (he : ∀ n, r (2*n) = t (2*n))
121     (hv : ∀ n, innovation X Y L r n = innovation X Y L t n) : r = t := by
122   apply lp.ext
123   apply BoundedParity.family_ext
124   · exact he
125   · intro n
126     rw [reconstruct_odd X Y hX hY L r n, reconstruct_odd X Y hX hY L t n, hc, he n, hv n]
127 
128 /-- Produce a residual family from independent bounded coarse and detail channels. -/
129 def synthesize (c : Coarse X Y hX hY) (a : EvenResidual X Y) (b : OddResidual X Y) :
130     Residuals X Y := hidden X Y hX hY L (BoundedParity.merge (a,b)) + lift X Y hX hY L c
131 
132 @[simp] theorem synthesize_coarse (c : Coarse X Y hX hY) (a : EvenResidual X Y)
133     (b : OddResidual X Y) : coarsen X Y hX hY (synthesize X Y hX hY L c a b) = c := by
134   unfold synthesize
135   rw [map_add, hidden_coarsen, coarsen_lift, zero_add]
136 
137 @[simp] theorem synthesize_even (c : Coarse X Y hX hY) (a : EvenResidual X Y)
138     (b : OddResidual X Y) (n : ℕ) : synthesize X Y hX hY L c a b (2*n) = a n := by
139   change hidden X Y hX hY L (BoundedParity.merge (a,b)) (2*n) + lift X Y hX hY L c (2*n) = _
140   rw [hidden_even, lift_even, BoundedParity.merge_even, add_zero]
141 
142 theorem synthesize_innovation (c : Coarse X Y hX hY) (a : EvenResidual X Y)
143     (b : OddResidual X Y) (hb : ∀ n, (Y.down (2*n)).comp (b n) = 0) (n : ℕ) :
144     innovation X Y L (synthesize X Y hX hY L c a b) n = b n := by
145   unfold synthesize
146   rw [innovation_add, innovation_hidden, innovation_lift, add_zero]
147   unfold innovation
148   rw [BoundedParity.merge_odd, hb n]
149   simp
150 
151 /-- The reconstructed odd edge uses the vertical kernel detail b and the even detail a. -/
152 theorem synthesize_odd (c : Coarse X Y hX hY) (a : EvenResidual X Y)
153     (b : OddResidual X Y) (hb : ∀ n, (Y.down (2*n)).comp (b n) = 0) (n : ℕ) :
154     synthesize X Y hX hY L c a b (2*n+1) =
155       b n + (L.up (2*n)).comp (c n - (a n).comp (X.down (2*n+1))) := by
156   rw [reconstruct_odd X Y hX hY L, synthesize_innovation X Y hX hY L c a b hb,
157     synthesize_coarse, synthesize_even]
158 
159 /-- Existence and uniqueness for all independent bounded channels. -/
160 theorem unique_synthesis (c : Coarse X Y hX hY) (a : EvenResidual X Y)
161     (b : OddResidual X Y) (hb : ∀ n, (Y.down (2*n)).comp (b n) = 0) :
162     ∃! r : Residuals X Y, coarsen X Y hX hY r = c ∧
163       (∀ n, r (2*n) = a n) ∧ (∀ n, innovation X Y L r n = b n) := by
164   refine ⟨synthesize X Y hX hY L c a b, ⟨synthesize_coarse X Y hX hY L c a b,
165     synthesize_even X Y hX hY L c a b, synthesize_innovation X Y hX hY L c a b hb⟩, ?_⟩
166   intro r hr
167   apply channels_injective X Y hX hY L
168   · rw [hr.1, synthesize_coarse]
169   · intro n; rw [hr.2.1 n, synthesize_even]
170   · intro n; rw [hr.2.2 n, synthesize_innovation X Y hX hY L c a b hb]
171 
172 /-- A channel budget is a rigorous bound on the reconstructed fine residual. -/
173 theorem synthesize_bound (c : Coarse X Y hX hY) (a : EvenResidual X Y)
174     (b : OddResidual X Y) :
175     ‖synthesize X Y hX hY L c a b‖ ≤
176       (1+2*(L.bound : ℝ))*max ‖a‖ ‖b‖ + (L.bound : ℝ)*‖c‖ := by
177   have hh := hidden_bound X Y hX hY L (BoundedParity.merge (a,b))
178   have hj := lift_bound X Y hX hY L c
179   have hm := BoundedParity.merge_bound (E := fun n => X.Obj (n+1) →L[𝕜] Y.Obj n) (a,b)
180   have ha := norm_add_le (hidden X Y hX hY L (BoundedParity.merge (a,b)))
181     (lift X Y hX hY L c)
182   change ‖BoundedParity.merge (E := fun n => X.Obj (n+1) →L[𝕜] Y.Obj n) (a,b)‖ ≤ max ‖a‖ ‖b‖ at hm
183   change ‖synthesize X Y hX hY L c a b‖ ≤ _ at ha
184   have hs : 0 ≤ (L.bound : ℝ) := NNReal.coe_nonneg _
185   nlinarith only [hh, hj, hm, ha, hs]
186 
187 /-- The possible vertical detail values form the kernel of target restriction. -/
188 def verticalSpace : Submodule 𝕜 (OddResidual X Y) where
189   carrier b := ∀ n, (Y.down (2*n)).comp (b n) = 0
190   zero_mem' := by intro n; simp
191   add_mem' := by
192     intro a b ha hb n
193     change (Y.down (2*n)).comp (a n + b n) = 0
194     rw [ContinuousLinearMap.comp_add, ha n, hb n, add_zero]
195   smul_mem' := by
196     intro c b hb n
197     change (Y.down (2*n)).comp (c • b n) = 0
198     rw [ContinuousLinearMap.comp_smul, hb n, smul_zero]
199 
200 /-- Explicit linear coordinates with independently selectable admissible detail channels. -/
201 def channelsLinear : Residuals X Y ≃ₗ[𝕜]
202     ((EvenResidual X Y × verticalSpace X Y) × Coarse X Y hX hY) where
203   toFun r := ((BoundedParity.even r, ⟨innovationFamily X Y hY L r, innovation_down X Y L r⟩),
204     coarsen X Y hX hY r)
205   invFun z := synthesize X Y hX hY L z.2 z.1.1 z.1.2.val
206   left_inv r := by
207     apply channels_injective X Y hX hY L
208     · exact synthesize_coarse X Y hX hY L _ _ _
209     · intro n; exact synthesize_even X Y hX hY L _ _ _ n
210     · intro n
211       exact synthesize_innovation X Y hX hY L
212         (coarsen X Y hX hY r) (BoundedParity.even r)
213         (innovationFamily X Y hY L r) (innovation_down X Y L r) n
214   right_inv z := by
215     apply Prod.ext
216     · apply Prod.ext
217       · apply lp.ext; funext n; exact synthesize_even X Y hX hY L _ _ _ n
218       · apply Subtype.ext; apply lp.ext; funext n
219         exact synthesize_innovation X Y hX hY L _ _ _ z.1.2.property n
220     · exact synthesize_coarse X Y hX hY L _ _ _
221   map_add' r t := by
222     apply Prod.ext
223     · apply Prod.ext
224       · apply lp.ext; rfl
225       · apply Subtype.ext; apply lp.ext; funext n; exact innovation_add X Y L r t n
226     · exact map_add (coarsen X Y hX hY) r t
227   map_smul' a r := by
228     apply Prod.ext
229     · apply Prod.ext
230       · apply lp.ext; rfl
231       · apply Subtype.ext; apply lp.ext; funext n; exact innovation_smul X Y L a r n
232     · exact map_smul (coarsen X Y hX hY) a r
233 
234 theorem channels_bound (r : Residuals X Y) :
235     ‖channelsLinear X Y hX hY L r‖ ≤ max (1+(L.bound : ℝ)) 2 * ‖r‖ := by
236   have he := BoundedParity.even_bound r
237   have hv := innovationFamily_bound X Y hY L r
238   have hc := residualSampleCLM_bound X Y hX hY schedule schedule_monotone 2 schedule_gap r
239   change ‖coarsen X Y hX hY r‖ ≤ 2*‖r‖ at hc
240   change max (max ‖BoundedParity.even r‖ ‖innovationFamily X Y hY L r‖)
241     ‖coarsen X Y hX hY r‖ ≤ _
242   have hs : 0 ≤ (L.bound : ℝ) := NNReal.coe_nonneg _
243   have hr : 0 ≤ ‖r‖ := norm_nonneg r
244   have hk1 : 1+(L.bound : ℝ) ≤ max (1+(L.bound : ℝ)) 2 := le_max_left _ _
245   have hk2 : 2 ≤ max (1+(L.bound : ℝ)) 2 := le_max_right _ _
246   apply max_le
247   · apply max_le <;> nlinarith only [he, hv, hs, hr, hk1, hk2]
248   · nlinarith only [hc, hr, hk2]
249 
250 theorem channels_inverse_bound (z : (EvenResidual X Y × verticalSpace X Y) × Coarse X Y hX hY) :
251     ‖(channelsLinear X Y hX hY L).symm z‖ ≤ (1+3*(L.bound : ℝ))*‖z‖ := by
252   have h := synthesize_bound X Y hX hY L z.2 z.1.1 z.1.2.val
253   have hd : max ‖z.1.1‖ ‖z.1.2.val‖ ≤ ‖z‖ := le_max_left _ _
254   have hc : ‖z.2‖ ≤ ‖z‖ := le_max_right _ _
255   have hs : 0 ≤ (L.bound : ℝ) := NNReal.coe_nonneg _
256   change ‖synthesize X Y hX hY L z.2 z.1.1 z.1.2.val‖ ≤ _
257   nlinarith only [h, hd, hc, hs]
258 
259 /-- No hidden residual is discarded: this is a bounded linear isomorphism. -/
260 def channels : Residuals X Y ≃L[𝕜]
261     ((EvenResidual X Y × verticalSpace X Y) × Coarse X Y hX hY) :=
262   (channelsLinear X Y hX hY L).toContinuousLinearEquivOfBounds
263     (max (1+(L.bound : ℝ)) 2) (1+3*(L.bound : ℝ))
264     (channels_bound X Y hX hY L) (channels_inverse_bound X Y hX hY L)
265 
266 
267 end DyadicResidual
268 end KomorebiSpace
269 end

Back to source controls