SplitTowerRepair.lean

1 import KomorebiSpace.BanachTowerExactification
2 
3 set_option autoImplicit false
4 
5 /-!
6 # A constructed right inverse for the tower differential
7 
8 The target bonding maps have uniformly bounded right inverses. A strict bound
9 on forward propagation makes the causal correction uniformly bounded. No
10 correction operator, exact candidate, or limiting repair is postulated.
11 -/
12 universe u v
13 noncomputable section
14 open scoped NNReal ENNReal
15 namespace KomorebiSpace
16 namespace BanachTower
17 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
18 variable (X Y : BanachTower.{u,v} 𝕜)
19 
20 /-- Chosen bounded splittings of the target bonding maps. -/
21 structure Splitting (Y : BanachTower.{u,v} 𝕜) where
22   up : ∀ n, Y.Obj n →L[𝕜] Y.Obj (n+1)
23   down_up : ∀ n, (Y.down n).comp (up n) = ContinuousLinearMap.id 𝕜 (Y.Obj n)
24   bound : ℝ≥0
25   up_bound : ∀ n, ‖up n‖ ≤ (bound : ℝ)
26 
27 namespace Splitting
28 variable {Y}
29 variable (L : Splitting Y)
30 
31 @[simp] theorem down_up_apply (n : ℕ) (y : Y.Obj n) :
32     Y.down n (L.up n y) = y :=
33   congrArg (fun T : Y.Obj n →L[𝕜] Y.Obj n => T y) (L.down_up n)
34 
35 def gain : ℝ := (L.bound : ℝ) / (1 - (L.bound : ℝ) * X.bound)
36 
37 variable (hgap : (L.bound : ℝ) * X.bound < 1)
38 
39 include hgap in
40 theorem gain_nonneg : 0 ≤ L.gain X := by
41   unfold gain
42   exact div_nonneg (NNReal.coe_nonneg _) (le_of_lt (sub_pos.mpr hgap))
43 
44 include hgap in
45 theorem gain_balance :
46     (L.bound : ℝ) * (1 + L.gain X * X.bound) = L.gain X := by
47   have hn : (1 - (L.bound : ℝ) * X.bound) ≠ 0 := ne_of_gt (sub_pos.mpr hgap)
48   unfold gain
49   field_simp [hn]
50   ring
51 
52 /-- The causal recurrence solving `d a = r` with `a 0 = 0`. -/
53 def rawCorrection (r : Residuals X Y) : ∀ n, X.Obj n →L[𝕜] Y.Obj n
54   | 0 => 0
55   | n+1 => (L.up n).comp (r n + (rawCorrection r n).comp (X.down n))
56 
57 @[simp] theorem rawCorrection_zero (r : Residuals X Y) : L.rawCorrection X r 0 = 0 := rfl
58 
59 @[simp] theorem rawCorrection_succ (r : Residuals X Y) (n : ℕ) :
60     L.rawCorrection X r (n+1) =
61       (L.up n).comp (r n + (L.rawCorrection X r n).comp (X.down n)) := rfl
62 
63 include hgap in
64 theorem rawCorrection_bound (r : Residuals X Y) (n : ℕ) :
65     ‖L.rawCorrection X r n‖ ≤ L.gain X * ‖r‖ := by
66   induction n with
67   | zero => simpa using mul_nonneg (L.gain_nonneg X hgap) (norm_nonneg r)
68   | succ n ih =>
69     have hr := lp.norm_apply_le_norm ENNReal.top_ne_zero r n
70     have ha : ‖(L.rawCorrection X r n).comp (X.down n)‖ ≤
71         (L.gain X * ‖r‖) * (X.bound : ℝ) :=
72       ((L.rawCorrection X r n).opNorm_comp_le _).trans
73         (mul_le_mul ih (X.down_bound n) (norm_nonneg _) (mul_nonneg
74           (L.gain_nonneg X hgap) (norm_nonneg r)))
75     calc
76       ‖L.rawCorrection X r (n+1)‖ ≤ ‖L.up n‖ *
77           ‖r n + (L.rawCorrection X r n).comp (X.down n)‖ :=
78         (L.up n).opNorm_comp_le _
79       _ ≤ (L.bound : ℝ) * ‖r n + (L.rawCorrection X r n).comp (X.down n)‖ :=
80         mul_le_mul_of_nonneg_right (L.up_bound n) (norm_nonneg _)
81       _ ≤ (L.bound : ℝ) * (‖r n‖ + ‖(L.rawCorrection X r n).comp (X.down n)‖) :=
82         mul_le_mul_of_nonneg_left (norm_add_le _ _) (NNReal.coe_nonneg _)
83       _ ≤ (L.bound : ℝ) * (‖r‖ + (L.gain X * ‖r‖) * (X.bound : ℝ)) :=
84         mul_le_mul_of_nonneg_left (add_le_add hr ha) (NNReal.coe_nonneg _)
85       _ = ((L.bound : ℝ) * (1 + L.gain X * X.bound)) * ‖r‖ := by ring
86       _ = L.gain X * ‖r‖ := by rw [L.gain_balance X hgap]
87 
88 theorem rawCorrection_add (r t : Residuals X Y) (n : ℕ) :
89     L.rawCorrection X (r+t) n = L.rawCorrection X r n + L.rawCorrection X t n := by
90   induction n with
91   | zero => simp
92   | succ n ih =>
93     rw [rawCorrection_succ, rawCorrection_succ, rawCorrection_succ, ih]
94     ext x
95     simp only [ContinuousLinearMap.comp_apply, add_apply,
96       lp.coeFn_add, Pi.add_apply, map_add]
97     abel
98 
99 theorem rawCorrection_smul (c : 𝕜) (r : Residuals X Y) (n : ℕ) :
100     L.rawCorrection X (c • r) n = c • L.rawCorrection X r n := by
101   induction n with
102   | zero => simp
103   | succ n ih =>
104     rw [rawCorrection_succ, rawCorrection_succ, ih]
105     ext x
106     simp [smul_add]
107 
108 include hgap in
109 theorem rawCorrection_mem (r : Residuals X Y) :
110     Memℓp (L.rawCorrection X r) (∞ : ℝ≥0∞) := by
111   apply memℓp_infty
112   refine ⟨L.gain X * ‖r‖, ?_⟩
113   rintro _ ⟨n, rfl⟩
114   exact L.rawCorrection_bound X hgap r n
115 
116 def correctionLinear : Residuals X Y →ₗ[𝕜] Candidates X Y where
117   toFun r := ⟨L.rawCorrection X r, L.rawCorrection_mem X hgap r⟩
118   map_add' r t := by
119     apply lp.ext
120     funext n
121     exact L.rawCorrection_add X r t n
122   map_smul' c r := by
123     apply lp.ext
124     funext n
125     exact L.rawCorrection_smul X c r n
126 
127 theorem correctionLinear_bound (r : Residuals X Y) :
128     ‖L.correctionLinear X hgap r‖ ≤ L.gain X * ‖r‖ := by
129   apply lp.norm_le_of_forall_le (mul_nonneg (L.gain_nonneg X hgap) (norm_nonneg r))
130   exact L.rawCorrection_bound X hgap r
131 
132 /-- A bounded right inverse, constructed from the bonding-map splittings. -/
133 def correction : Residuals X Y →L[𝕜] Candidates X Y :=
134   (L.correctionLinear X hgap).mkContinuous (L.gain X)
135     (L.correctionLinear_bound X hgap)
136 
137 @[simp] theorem correction_apply (r : Residuals X Y) (n : ℕ) :
138     L.correction X hgap r n = L.rawCorrection X r n := rfl
139 
140 theorem correction_bound (r : Residuals X Y) :
141     ‖L.correction X hgap r‖ ≤ L.gain X * ‖r‖ := L.correctionLinear_bound X hgap r
142 
143 theorem correction_opNorm : ‖L.correction X hgap‖ ≤ L.gain X :=
144   ContinuousLinearMap.opNorm_le_bound _ (L.gain_nonneg X hgap)
145     (L.correction_bound X hgap)
146 
147 theorem rawCorrection_defect (r : Residuals X Y) (n : ℕ) :
148     (Y.down n).comp (L.rawCorrection X r (n+1)) -
149       (L.rawCorrection X r n).comp (X.down n) = r n := by
150   ext x
151   simp [rawCorrection_succ]
152 
153 /-- Exact cancellation on every bounded residual, not only those already in the range. -/
154 @[simp] theorem differential_correction (r : Residuals X Y) :
155     differential X Y (L.correction X hgap r) = r := by
156   apply lp.ext
157   funext n
158   exact L.rawCorrection_defect X r n
159 
160 @[simp] theorem correction_preserves_zero (r : Residuals X Y) :
161     L.correction X hgap r 0 = 0 := rfl
162 
163 /-- The constructed correction discharges all hypotheses of the existing repair engine. -/
164 def scheme : RepairDynamics.Scheme (differential X Y) (evaluation X Y 0) where
165   correction := L.correction X hgap
166   rate := 0
167   rate_nonneg := le_rfl
168   rate_lt_one := zero_lt_one
169   preserve r := rfl
170   contract f := by simp
171 
172 /-- The exactifier has a finite formula, independent of limit packaging. -/
173 def repair : Candidates X Y →L[𝕜] Candidates X Y :=
174   ContinuousLinearMap.id 𝕜 _ - (L.correction X hgap).comp (differential X Y)
175 
176 @[simp] theorem repair_apply (f : Candidates X Y) :
177     L.repair X hgap f = f - L.correction X hgap (differential X Y f) := rfl
178 
179 @[simp] theorem repair_differential_zero (f : Candidates X Y) :
180     differential X Y (L.repair X hgap f) = 0 := by
181   simp only [repair_apply, map_sub, differential_correction, sub_self]
182 
183 theorem repair_exact (f : Candidates X Y) : Exact X Y (L.repair X hgap f) :=
184   (exact_iff_differential_zero X Y _).mpr (L.repair_differential_zero X hgap f)
185 
186 @[simp] theorem repair_preserves_zero (f : Candidates X Y) :
187     L.repair X hgap f 0 = f 0 := by
188   change f 0 - L.correction X hgap (differential X Y f) 0 = f 0
189   simp
190 
191 @[simp] theorem repair_fixes_exact (f : Candidates X Y) (hf : Exact X Y f) :
192     L.repair X hgap f = f := by
193   rw [repair_apply, (exact_iff_differential_zero X Y f).mp hf, map_zero, sub_zero]
194 
195 @[simp] theorem repair_idempotent (f : Candidates X Y) :
196     L.repair X hgap (L.repair X hgap f) = L.repair X hgap f :=
197   L.repair_fixes_exact X hgap _ (L.repair_exact X hgap f)
198 
199 theorem repair_error (f : Candidates X Y) :
200     ‖f - L.repair X hgap f‖ ≤ L.gain X * ‖differential X Y f‖ := by
201   rw [repair_apply, sub_sub_cancel]
202   exact L.correction_bound X hgap _
203 
204 theorem repair_image_iff (g : Candidates X Y) :
205     (∃ f, L.repair X hgap f = g) ↔ Exact X Y g := by
206   constructor
207   · rintro ⟨f, rfl⟩
208     exact L.repair_exact X hgap f
209   · intro hg
210     exact ⟨g, L.repair_fixes_exact X hgap g hg⟩
211 
212 /-- The abstract limiting projector equals the explicit one-step repair. -/
213 theorem scheme_projection_eq (f : Candidates X Y) :
214     (L.scheme X hgap).projection f = L.repair X hgap f := by
215   have h := ((L.scheme X hgap).limit_spec f).2.2.2 1
216   have hstep : RepairDynamics.orbit (differential X Y) (L.scheme X hgap).correction f 1 =
217       L.repair X hgap f := rfl
218   rw [hstep, L.repair_differential_zero X hgap, norm_zero, mul_zero] at h
219   exact (dist_le_zero.mp h).symm
220 
221 end Splitting
222 end BanachTower
223 end KomorebiSpace
224 end

Back to source controls