SplitKernelPerturbation.lean

1 import KomorebiSpace.MovingKernelBounds
2 import Mathlib.Analysis.SpecificLimits.Normed
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Small perturbations of a split-surjective defect
8 
9 A bounded right inverse of d is an explicit input. A Neumann inverse on the
10 residual space constructs a right inverse of e when a*epsilon<1. The perturbed
11 residual bound and kernel comparison are conclusions: no preservation of the
12 old kernel is assumed. The graph comparison is relative to the chosen splitting.
13 -/
14 universe u v
15 noncomputable section
16 namespace KomorebiSpace
17 namespace SplitKernel
18 open HilbertKernelProjection
19 variable {E : Type u} {R : Type v}
20 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
21 variable [NormedAddCommGroup R] [NormedSpace ℝ R] [CompleteSpace R]
22 variable (d e : E →L[ℝ] R)
23 
24 structure Certificate where
25   sectionMap : R →L[ℝ] E
26   right_inverse : ∀ r, d (sectionMap r) = r
27   constant : ℝ
28   nonneg : 0 ≤ constant
29   section_bound : ∀ r, ‖sectionMap r‖ ≤ constant*‖r‖
30   epsilon : ℝ
31   epsilon_nonneg : 0 ≤ epsilon
32   operator_error : ‖d-e‖ ≤ epsilon
33   small : constant*epsilon < 1
34 
35 namespace Certificate
36 variable {d e} (T : Certificate d e)
37 
38 /-- Error in the old residual-coordinate section. -/
39 def residualError : R →L[ℝ] R := (d-e).comp T.sectionMap
40 
41 omit [CompleteSpace E] [CompleteSpace R] in
42 theorem residualError_bound : ‖T.residualError‖ ≤ T.constant*T.epsilon := by
43   apply ContinuousLinearMap.opNorm_le_bound _ (mul_nonneg T.nonneg T.epsilon_nonneg)
44   intro r
45   change ‖(d-e) (T.sectionMap r)‖ ≤ _
46   calc
47     _ ≤ ‖d-e‖*‖T.sectionMap r‖ := (d-e).le_opNorm _
48     _ ≤ T.epsilon*(T.constant*‖r‖) :=
49       mul_le_mul T.operator_error (T.section_bound r) (norm_nonneg _) T.epsilon_nonneg
50     _ = _ := by ring
51 
52 omit [CompleteSpace E] [CompleteSpace R] in
53 theorem residualError_small : ‖T.residualError‖ < 1 :=
54   T.residualError_bound.trans_lt T.small
55 
56 /-- A genuine invertible residual-coordinate map, constructed by a geometric series. -/
57 def residualEquiv : R ≃L[ℝ] R :=
58   ContinuousLinearEquiv.ofUnit (Units.oneSub T.residualError T.residualError_small)
59 
60 omit [CompleteSpace E] in
61 @[simp] theorem residualEquiv_apply (r : R) : T.residualEquiv r = e (T.sectionMap r) := by
62   change r-(d-e) (T.sectionMap r)=_
63   rw [sub_apply,T.right_inverse]
64   abel
65 
66 omit [CompleteSpace E] in
67 /-- The inverse norm is derived from the strict radius, not supplied separately. -/
68 theorem residual_inverse_bound (r : R) :
69     ‖T.residualEquiv.symm r‖ ≤ (1/(1-T.constant*T.epsilon))*‖r‖ := by
70   let z := T.residualEquiv.symm r
71   have hid : z = r+T.residualError z := by
72     have hi := T.residualEquiv.apply_symm_apply r
73     change z-T.residualError z = r at hi
74     exact (sub_eq_iff_eq_add).mp hi
75   have hz : ‖z‖ ≤ ‖r‖+(T.constant*T.epsilon)*‖z‖ := by
76     calc
77       ‖z‖ = ‖r+T.residualError z‖ := congrArg norm hid
78       _ ≤ ‖r‖+‖T.residualError z‖ := norm_add_le _ _
79       _ ≤ _ := add_le_add le_rfl ((T.residualError.le_opNorm z).trans
80         (mul_le_mul_of_nonneg_right T.residualError_bound (norm_nonneg z)))
81   have hp : 0 < 1-T.constant*T.epsilon := sub_pos.mpr T.small
82   have hh : (1-T.constant*T.epsilon)*‖z‖ ≤ ‖r‖ := by nlinarith
83   calc
84     ‖z‖ ≤ ‖r‖/(1-T.constant*T.epsilon) := (le_div_iff₀ hp).mpr (by nlinarith [hh])
85     _ = _ := by ring
86 
87 /-- The perturbed right inverse retains the old section range. -/
88 def perturbedSection : R →L[ℝ] E :=
89   T.sectionMap.comp T.residualEquiv.symm.toContinuousLinearMap
90 
91 omit [CompleteSpace E] in
92 @[simp] theorem perturbed_right_inverse (r : R) : e (T.perturbedSection r) = r := by
93   change e (T.sectionMap (T.residualEquiv.symm r)) = r
94   rw [← T.residualEquiv_apply]
95   exact T.residualEquiv.apply_symm_apply r
96 
97 omit [CompleteSpace E] in
98 theorem perturbed_section_bound (r : R) :
99     ‖T.perturbedSection r‖ ≤ (T.constant/(1-T.constant*T.epsilon))*‖r‖ := by
100   exact (T.section_bound _).trans (by
101     calc
102       T.constant*‖T.residualEquiv.symm r‖ ≤
103           T.constant*((1/(1-T.constant*T.epsilon))*‖r‖) :=
104         mul_le_mul_of_nonneg_left (T.residual_inverse_bound r) T.nonneg
105       _ = _ := by ring)
106 
107 include T in
108 omit [CompleteSpace E] in
109 theorem perturbed_surjective : Function.Surjective e :=
110   fun r => ⟨T.perturbedSection r, T.perturbed_right_inverse r⟩
111 
112 /-- A right inverse supplies an exact competitor, hence an orthogonal repair bound. -/
113 def referenceBound : ResidualRobustness.Bound d where
114   constant := T.constant
115   nonneg := T.nonneg
116   estimate x := by
117     have hx : d (x-T.sectionMap (d x))=0 := by rw [map_sub,T.right_inverse,sub_self]
118     have hb := projection_best d x (x-T.sectionMap (d x)) hx
119     have hid : x-(x-T.sectionMap (d x))=T.sectionMap (d x) := by abel
120     rw [hid] at hb
121     exact hb.trans (T.section_bound _)
122 
123 def perturbedBound : ResidualRobustness.Bound e where
124   constant := T.constant/(1-T.constant*T.epsilon)
125   nonneg := div_nonneg T.nonneg (le_of_lt (sub_pos.mpr T.small))
126   estimate x := by
127     have hx : e (x-T.perturbedSection (e x))=0 := by
128       rw [map_sub,T.perturbed_right_inverse,sub_self]
129     have hb := projection_best e x (x-T.perturbedSection (e x)) hx
130     have hid : x-(x-T.perturbedSection (e x))=T.perturbedSection (e x) := by abel
131     rw [hid] at hb
132     exact hb.trans (T.perturbed_section_bound _)
133 
134 include T in
135 theorem perturbed_range_closed : IsClosed (Set.range e) :=
136   closed_range_of_bound e T.perturbedBound.constant T.perturbedBound.nonneg
137     T.perturbedBound.estimate
138 
139 /-- A one-certificate motion bound; the new stability constant has been derived. -/
140 theorem projection_motion :
141     ‖projection d-projection e‖ ≤
142       (T.constant*T.epsilon)/(1-T.constant*T.epsilon) := by
143   have hp : 0 < 1-T.constant*T.epsilon := sub_pos.mpr T.small
144   have hc : T.constant ≤ T.constant/(1-T.constant*T.epsilon) := by
145     apply (le_div_iff₀ hp).mpr
146     nlinarith [mul_nonneg (mul_nonneg T.nonneg T.epsilon_nonneg) T.nonneg]
147   have hb := MovingKernel.projection_opNorm d e T.referenceBound T.perturbedBound T.operator_error
148   change ‖projection d-projection e‖ ≤ max T.constant
149     (T.constant/(1-T.constant*T.epsilon))*T.epsilon at hb
150   rw [max_eq_right hc] at hb
151   convert hb using 1
152   ring
153 
154 /-- A literal old-kernel-preservation assumption is absent from this estimate. -/
155 theorem perturbed_measured (x : E) (r : R) (η : ℝ) (hr : ‖e x-r‖ ≤ η) :
156     ‖x-projection e x‖ ≤ (T.constant/(1-T.constant*T.epsilon))*(‖r‖+η) :=
157   T.perturbedBound.measured x r η hr
158 
159 /-- The old splitting projection, not necessarily orthogonal. -/
160 def oldRetract : E →L[ℝ] E := ContinuousLinearMap.id ℝ E - T.sectionMap.comp d
161 
162 /-- The new splitting projection; its kernel complement is the old section range. -/
163 def newRetract : E →L[ℝ] E := ContinuousLinearMap.id ℝ E - T.perturbedSection.comp e
164 
165 omit [CompleteSpace E] [CompleteSpace R] in
166 @[simp] theorem oldRetract_apply (x : E) : T.oldRetract x = x-T.sectionMap (d x) := rfl
167 omit [CompleteSpace E] in
168 @[simp] theorem newRetract_apply (x : E) : T.newRetract x = x-T.perturbedSection (e x) := rfl
169 
170 omit [CompleteSpace E] [CompleteSpace R] in
171 @[simp] theorem oldRetract_exact (x : E) : d (T.oldRetract x)=0 := by
172   rw [T.oldRetract_apply,map_sub,T.right_inverse,sub_self]
173 
174 omit [CompleteSpace E] in
175 @[simp] theorem newRetract_exact (x : E) : e (T.newRetract x)=0 := by
176   rw [T.newRetract_apply,map_sub,T.perturbed_right_inverse,sub_self]
177 
178 omit [CompleteSpace E] in
179 @[simp] theorem section_cancel (r : R) : T.perturbedSection (e (T.sectionMap r))=T.sectionMap r := by
180   change T.sectionMap (T.residualEquiv.symm (e (T.sectionMap r)))=_
181   rw [← T.residualEquiv_apply,T.residualEquiv.symm_apply_apply]
182 
183 omit [CompleteSpace E] in
184 @[simp] theorem oldRetract_newSection (r : R) : T.oldRetract (T.perturbedSection r)=0 := by
185   change T.sectionMap (T.residualEquiv.symm r)-
186     T.sectionMap (d (T.sectionMap (T.residualEquiv.symm r)))=0
187   rw [T.right_inverse,sub_self]
188 
189 omit [CompleteSpace E] in
190 @[simp] theorem newRetract_oldSection (r : R) : T.newRetract (T.sectionMap r)=0 := by
191   rw [T.newRetract_apply,T.section_cancel,sub_self]
192 
193 def toNewKernel : d.ker →L[ℝ] e.ker :=
194   (T.newRetract.comp d.ker.subtypeL).codRestrict e.ker (fun x => T.newRetract_exact x)
195 
196 def toOldKernel : e.ker →L[ℝ] d.ker :=
197   (T.oldRetract.comp e.ker.subtypeL).codRestrict d.ker (fun x => T.oldRetract_exact x)
198 
199 omit [CompleteSpace E] in
200 theorem toOld_toNew (x : d.ker) : T.toOldKernel (T.toNewKernel x)=x := by
201   apply Subtype.ext
202   change T.oldRetract (T.newRetract x.val)=x.val
203   have hx : d x.val = 0 := x.property
204   rw [T.newRetract_apply,map_sub,T.oldRetract_newSection,sub_zero,
205     T.oldRetract_apply,hx,map_zero,sub_zero]
206 
207 omit [CompleteSpace E] in
208 theorem toNew_toOld (x : e.ker) : T.toNewKernel (T.toOldKernel x)=x := by
209   apply Subtype.ext
210   change T.newRetract (T.oldRetract x.val)=x.val
211   have hx : e x.val = 0 := x.property
212   rw [T.oldRetract_apply,map_sub,T.newRetract_oldSection,sub_zero,
213     T.newRetract_apply,hx,map_zero,sub_zero]
214 
215 /-- Actual continuously invertible transport between the moving exact spaces. -/
216 def kernelEquiv : d.ker ≃L[ℝ] e.ker where
217   toLinearEquiv :=
218     { T.toNewKernel.toLinearMap with
219       invFun := T.toOldKernel
220       left_inv := T.toOld_toNew
221       right_inv := T.toNew_toOld }
222   continuous_toFun := T.toNewKernel.continuous
223   continuous_invFun := T.toOldKernel.continuous
224 
225 /-- The new exact object is close to the old one in the declared ambient norm. -/
226 theorem kernel_transport_error (x : d.ker) :
227     ‖(T.kernelEquiv x).val-x.val‖ ≤
228       ((T.constant*T.epsilon)/(1-T.constant*T.epsilon))*‖x.val‖ := by
229   change ‖(x.val-T.perturbedSection (e x.val))-x.val‖ ≤ _
230   have hid : (x.val-T.perturbedSection (e x.val))-x.val = -T.perturbedSection (e x.val) := by abel
231   rw [hid,norm_neg]
232   have hd : ‖e x.val‖ ≤ T.epsilon*‖x.val‖ := by
233     have he := ((d-e).le_opNorm x.val).trans
234       (mul_le_mul_of_nonneg_right T.operator_error (norm_nonneg x.val))
235     have hx : d x.val = 0 := x.property
236     simpa only [sub_apply,hx,zero_sub,norm_neg] using he
237   exact (T.perturbed_section_bound _).trans (by
238     calc
239       (T.constant/(1-T.constant*T.epsilon))*‖e x.val‖ ≤
240           (T.constant/(1-T.constant*T.epsilon))*(T.epsilon*‖x.val‖) :=
241         mul_le_mul_of_nonneg_left hd T.perturbedBound.nonneg
242       _ = _ := by ring)
243 
244 end Certificate
245 end SplitKernel
246 end KomorebiSpace
247 end

Back to source controls