DyadicResidualHierarchy.lean

1 import KomorebiSpace.DyadicResidualSplit
2 import KomorebiSpace.CoarseningCascade
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Actual iterated dyadic residual reconstruction
8 
9 The target splitting is constructed at each coarser resolution by composition.
10 Consequently every finite depth has a lossless residual hierarchy. There is
11 no assertion of uniform bounds or convergence at infinite depth.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace DyadicResidual
17 open BanachTower
18 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
19 variable (Y : BanachTower.{u,v} 𝕜) (hY : ∀ n, ‖Y.down n‖ ≤ 1) (L : Splitting Y)
20 
21 /-- Target sections remain available after pairing, by composing adjacent sections. -/
22 def sampledSplitting : Splitting (sampled Y hY) where
23   up n := (L.up (2*n+1)).comp (L.up (2*n))
24   down_up n := by
25     change (restriction Y (show 2*n ≤ 2*(n+1) from schedule_monotone (Nat.le_succ n))).comp
26       ((L.up (2*n+1)).comp (L.up (2*n))) = ContinuousLinearMap.id 𝕜 (Y.Obj (2*n))
27     rw [restriction_succ Y (show 2*n ≤ 2*n+1 by omega), restriction_adjacent]
28     ext y
29     change Y.down (2*n) (Y.down (2*n+1) (L.up (2*n+1) (L.up (2*n) y))) = y
30     rw [L.down_up_apply, L.down_up_apply]
31   bound := L.bound * L.bound
32   up_bound n := by
33     exact ((L.up (2*n+1)).opNorm_comp_le (L.up (2*n))).trans
34       (mul_le_mul (L.up_bound _) (L.up_bound _) (norm_nonneg _) (NNReal.coe_nonneg _))
35 
36 /-- The full input to one genuine dyadic residual map. -/
37 structure System (𝕜 : Type u) [NontriviallyNormedField 𝕜] where
38   source : BanachTower.{u,v} 𝕜
39   target : BanachTower.{u,v} 𝕜
40   source_contractive : ∀ n, ‖source.down n‖ ≤ 1
41   target_contractive : ∀ n, ‖target.down n‖ ≤ 1
42   target_splitting : Splitting target
43 
44 namespace System
45 variable (T : System.{u,v} 𝕜)
46 
47 /-- Coarsen both actual towers on the same paired schedule. -/
48 def next : System.{u,v} 𝕜 where
49   source := sampled T.source T.source_contractive
50   target := sampled T.target T.target_contractive
51   source_contractive n := restriction_contractive T.source T.source_contractive
52     (schedule_monotone (Nat.le_succ n))
53   target_contractive n := restriction_contractive T.target T.target_contractive
54     (schedule_monotone (Nat.le_succ n))
55   target_splitting := sampledSplitting T.target T.target_contractive T.target_splitting
56 
57 def stage : ℕ → System.{u,v} 𝕜
58   | 0 => T
59   | n+1 => (stage n).next
60 
61 /-- This cascade uses the actual residual accumulation at every depth. -/
62 def cascade : CoarseningCascade.{u,v} 𝕜 where
63   Obj n := Residuals (T.stage n).source (T.stage n).target
64   down n := coarsen (T.stage n).source (T.stage n).target
65     (T.stage n).source_contractive (T.stage n).target_contractive
66   splitting n := sectionC (T.stage n).source (T.stage n).target
67     (T.stage n).source_contractive (T.stage n).target_contractive (T.stage n).target_splitting
68 
69 /-- No scalar-model substitution: reconstruction is on the original residual space. -/
70 theorem residual_reconstruction (r : Residuals T.source T.target) (N : ℕ) :
71     r = (∑ n ∈ Finset.range N, T.cascade.detailTerm r n) +
72       T.cascade.restore N (T.cascade.level r N) := T.cascade.reconstruction r N
73 
74 /-- Retained details plus the final coarse datum detect exactness at every finite depth. -/
75 theorem exactness_iff_hierarchy (f : Candidates T.source T.target) (N : ℕ) :
76     Exact T.source T.target f ↔
77       (∀ n < N, T.cascade.detail (differential T.source T.target f) n = 0) ∧
78       T.cascade.level (differential T.source T.target f) N = 0 := by
79   rw [exact_iff_differential_zero]
80   exact T.cascade.zero_iff _ N
81 
82 end System
83 end DyadicResidual
84 end KomorebiSpace
85 end

Back to source controls