SplitTowerPerturbation.lean

1 import KomorebiSpace.SplitTowerCanonicity
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Quantitative dependence on the target splitting
7 
8 The source and target towers remain fixed. Uniformly close right inverses of
9 the target bonding maps yield uniformly close correction operators, with an
10 explicit two-gap denominator. This is not invariance under changing norms.
11 -/
12 universe u v
13 noncomputable section
14 open scoped NNReal ENNReal
15 namespace KomorebiSpace
16 namespace BanachTower
17 namespace Splitting
18 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
19 variable (X : BanachTower.{u,v} 𝕜) {Y : BanachTower.{u,v} 𝕜}
20 variable (L M : Splitting Y)
21 
22 /-- The denominator records distance to the propagation threshold for both splittings. -/
23 def perturbationGain (ε : ℝ) : ℝ :=
24   ε / ((1 - (L.bound : ℝ) * X.bound) * (1 - (M.bound : ℝ) * X.bound))
25 
26 variable (hL : (L.bound : ℝ) * X.bound < 1)
27 variable (hM : (M.bound : ℝ) * X.bound < 1)
28 variable {ε : ℝ} (hε : 0 ≤ ε)
29 
30 include hL hM hε in
31  theorem perturbationGain_nonneg : 0 ≤ L.perturbationGain X M ε := by
32   exact div_nonneg hε (le_of_lt (mul_pos (sub_pos.mpr hL) (sub_pos.mpr hM)))
33 
34 include hL hM in
35  theorem perturbationGain_balance (ε : ℝ) :
36     (L.bound : ℝ) * (L.perturbationGain X M ε * X.bound) +
37       ε * (1 + M.gain X * X.bound) = L.perturbationGain X M ε := by
38   have hl : 1 - (L.bound : ℝ) * X.bound ≠ 0 := ne_of_gt (sub_pos.mpr hL)
39   have hm : 1 - (M.bound : ℝ) * X.bound ≠ 0 := ne_of_gt (sub_pos.mpr hM)
40   have hm' : 1 - (X.bound : ℝ) * M.bound ≠ 0 := by simpa only [mul_comm] using hm
41   unfold perturbationGain gain
42   field_simp [hl, hm, hm']
43   ring
44 
45 /-- Exact perturbation recurrence before any norm estimate. -/
46 theorem rawCorrection_difference_succ (r : Residuals X Y) (n : ℕ) :
47     L.rawCorrection X r (n+1) - M.rawCorrection X r (n+1) =
48       (L.up n).comp ((L.rawCorrection X r n - M.rawCorrection X r n).comp (X.down n)) +
49       (L.up n - M.up n).comp (r n + (M.rawCorrection X r n).comp (X.down n)) := by
50   rw [rawCorrection_succ, rawCorrection_succ]
51   ext x
52   simp only [ContinuousLinearMap.comp_apply, sub_apply, add_apply, map_add, map_sub]
53   abel
54 
55 include hL hM hε in
56  theorem rawCorrection_perturbation (hclose : ∀ n, ‖L.up n - M.up n‖ ≤ ε)
57     (r : Residuals X Y) (n : ℕ) :
58     ‖L.rawCorrection X r n - M.rawCorrection X r n‖ ≤
59       L.perturbationGain X M ε * ‖r‖ := by
60   have hc : 0 ≤ L.perturbationGain X M ε := L.perturbationGain_nonneg X M hL hM hε
61   induction n with
62   | zero => simpa using mul_nonneg hc (norm_nonneg r)
63   | succ n ih =>
64     have hn := lp.norm_apply_le_norm ENNReal.top_ne_zero r n
65     have hx : ‖(L.rawCorrection X r n - M.rawCorrection X r n).comp (X.down n)‖ ≤
66         (L.perturbationGain X M ε * ‖r‖) * (X.bound : ℝ) :=
67       ((L.rawCorrection X r n - M.rawCorrection X r n).opNorm_comp_le _).trans
68         (mul_le_mul ih (X.down_bound n) (norm_nonneg _) (mul_nonneg hc (norm_nonneg r)))
69     have hm : ‖(M.rawCorrection X r n).comp (X.down n)‖ ≤
70         (M.gain X * ‖r‖) * (X.bound : ℝ) :=
71       ((M.rawCorrection X r n).opNorm_comp_le _).trans
72         (mul_le_mul (M.rawCorrection_bound X hM r n) (X.down_bound n)
73           (norm_nonneg _) (mul_nonneg (M.gain_nonneg X hM) (norm_nonneg r)))
74     have ha : ‖(L.up n).comp
75         ((L.rawCorrection X r n - M.rawCorrection X r n).comp (X.down n))‖ ≤
76         (L.bound : ℝ) * ((L.perturbationGain X M ε * ‖r‖) * (X.bound : ℝ)) :=
77       ((L.up n).opNorm_comp_le _).trans
78         (mul_le_mul (L.up_bound n) hx (norm_nonneg _) (NNReal.coe_nonneg _))
79     have hb : ‖(L.up n - M.up n).comp (r n + (M.rawCorrection X r n).comp (X.down n))‖ ≤
80         ε * (‖r‖ + (M.gain X * ‖r‖) * (X.bound : ℝ)) :=
81       ((L.up n - M.up n).opNorm_comp_le _).trans
82         (mul_le_mul (hclose n) ((norm_add_le _ _).trans (add_le_add hn hm))
83           (norm_nonneg _) hε)
84     rw [L.rawCorrection_difference_succ X M r n]
85     calc
86       _ ≤ _ := norm_add_le _ _
87       _ ≤ (L.bound : ℝ) * ((L.perturbationGain X M ε * ‖r‖) * (X.bound : ℝ)) +
88           ε * (‖r‖ + (M.gain X * ‖r‖) * (X.bound : ℝ)) := add_le_add ha hb
89       _ = ((L.bound : ℝ) * (L.perturbationGain X M ε * X.bound) +
90           ε * (1 + M.gain X * X.bound)) * ‖r‖ := by ring
91       _ = _ := by rw [L.perturbationGain_balance X M hL hM]
92 
93 include hε in
94  theorem correction_perturbation (hclose : ∀ n, ‖L.up n - M.up n‖ ≤ ε)
95     (r : Residuals X Y) :
96     ‖L.correction X hL r - M.correction X hM r‖ ≤
97       L.perturbationGain X M ε * ‖r‖ := by
98   apply lp.norm_le_of_forall_le
99     (mul_nonneg (L.perturbationGain_nonneg X M hL hM hε) (norm_nonneg r))
100   intro n
101   exact L.rawCorrection_perturbation X M hL hM hε hclose r n
102 
103 include hε in
104  theorem correction_perturbation_opNorm (hclose : ∀ n, ‖L.up n - M.up n‖ ≤ ε) :
105     ‖L.correction X hL - M.correction X hM‖ ≤ L.perturbationGain X M ε := by
106   apply ContinuousLinearMap.opNorm_le_bound _ (L.perturbationGain_nonneg X M hL hM hε)
107   exact L.correction_perturbation X M hL hM hε hclose
108 
109 include hε in
110  theorem repair_perturbation (hclose : ∀ n, ‖L.up n - M.up n‖ ≤ ε)
111     (f : Candidates X Y) :
112     ‖M.repair X hM f - L.repair X hL f‖ ≤
113       L.perturbationGain X M ε * ‖differential X Y f‖ := by
114   rw [L.repair_change X M hL hM f]
115   exact L.correction_perturbation X M hL hM hε hclose _
116 
117 include hε in
118  theorem repair_perturbation_opNorm (hclose : ∀ n, ‖L.up n - M.up n‖ ≤ ε) :
119     ‖M.repair X hM - L.repair X hL‖ ≤
120       L.perturbationGain X M ε * ((X.bound : ℝ) + Y.bound) := by
121   have hc := L.perturbationGain_nonneg X M hL hM hε
122   apply ContinuousLinearMap.opNorm_le_bound _ (mul_nonneg hc (by positivity))
123   intro f
124   calc
125     _ ≤ L.perturbationGain X M ε * ‖differential X Y f‖ :=
126       L.repair_perturbation X M hL hM hε hclose f
127     _ ≤ L.perturbationGain X M ε * (((X.bound : ℝ) + Y.bound) * ‖f‖) :=
128       mul_le_mul_of_nonneg_left (differential_bound X Y f) hc
129     _ = _ := by ring
130 
131 end Splitting
132 end BanachTower
133 end KomorebiSpace
134 end

Back to source controls