MovingKernelBounds.lean

1 import KomorebiSpace.ResidualPerturbation
2 import Mathlib.Analysis.InnerProductSpace.Basic
3 import Mathlib.Tactic.Ring
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Controlled motion of actual exact spaces
9 
10 Two independently certified residual bounds control both directions of kernel
11 motion. Unlike the previous preserved-kernel theorem, neither kernel inclusion
12 is assumed. The comparison is between the actual orthogonal projections. The
13 operator-norm estimate uses the larger directional gain, not their sum.
14 -/
15 universe u v
16 noncomputable section
17 namespace KomorebiSpace
18 namespace MovingKernel
19 open HilbertKernelProjection
20 variable {E : Type u} {R : Type v}
21 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
22 variable [NormedAddCommGroup R] [NormedSpace ℝ R]
23 variable (d e : E →L[ℝ] R)
24 
25 /-- A bound on old exact vectors also controls projection of new-orthogonal vectors. -/
26 theorem complement_projection_bound {β : ℝ} (hβ : 0 ≤ β)
27     (h : ∀ z, d z = 0 → ‖z-projection e z‖ ≤ β*‖z‖)
28     (u : E) (hu : u ∈ e.kerᗮ) :
29     ‖projection d u‖ ≤ β*‖u‖ := by
30   let v := projection d u
31   have hv : d v = 0 := projection_exact d u
32   have h1 : inner ℝ v (u-v) = 0 := error_orthogonal d u v hv
33   have h2 : inner ℝ (projection e v) u = 0 := hu _ (projection_mem e v)
34   have hid : inner ℝ (v-projection e v) u = ‖v‖^2 := by
35     rw [inner_sub_left, h2, sub_zero]
36     rw [inner_sub_right, real_inner_self_eq_norm_sq] at h1
37     linarith
38   have hc : ‖v‖^2 ≤ (β*‖v‖)*‖u‖ := by
39     calc
40       ‖v‖^2 = inner ℝ (v-projection e v) u := hid.symm
41       _ ≤ ‖v-projection e v‖*‖u‖ := real_inner_le_norm _ _
42       _ ≤ (β*‖v‖)*‖u‖ := mul_le_mul_of_nonneg_right (h v hv) (norm_nonneg u)
43   by_cases hz : ‖v‖ = 0
44   · change ‖v‖ ≤ _
45     rw [hz]
46     positivity
47   · have hp : 0 < ‖v‖ := lt_of_le_of_ne (norm_nonneg v) (Ne.symm hz)
48     change ‖v‖ ≤ _
49     nlinarith
50 
51 /-- The two components of projection motion are orthogonal, hence a maximum bound. -/
52 theorem projection_motion_of_directional {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β)
53     (hnew : ∀ z, e z = 0 → ‖z-projection d z‖ ≤ α*‖z‖)
54     (hold : ∀ z, d z = 0 → ‖z-projection e z‖ ≤ β*‖z‖)
55     (x : E) :
56     ‖projection d x-projection e x‖ ≤ max α β * ‖x‖ := by
57   let u := x-projection e x
58   let v := projection e x
59   let w := projection d u
60   let z := v-projection d v
61   have hu : u ∈ e.kerᗮ := error_orthogonal e x
62   have hv : e v = 0 := projection_exact e x
63   have hw : d w = 0 := projection_exact d u
64   have hz : z ∈ d.kerᗮ := error_orthogonal d v
65   have horth : inner ℝ w z = 0 := hz w hw
66   have huv : inner ℝ u v = 0 := by
67     rw [real_inner_comm]
68     exact hu v hv
69   have hid : projection d x-projection e x = w-z := by
70     dsimp [w,z,u,v]
71     rw [map_sub]
72     abel
73   have hxid : x = u+v := by dsimp [u,v]; abel
74   have hsq : ‖projection d x-projection e x‖^2 = ‖w‖^2+‖z‖^2 := by
75     rw [hid,norm_sub_sq_real,horth]
76     ring
77   have hxnorm : ‖x‖^2 = ‖u‖^2+‖v‖^2 := by
78     rw [hxid,norm_add_sq_real,huv]
79     ring
80   have hwu : ‖w‖ ≤ max α β * ‖u‖ :=
81     (complement_projection_bound d e hβ hold u hu).trans
82       (mul_le_mul_of_nonneg_right (le_max_right α β) (norm_nonneg u))
83   have hzv : ‖z‖ ≤ max α β * ‖v‖ :=
84     (hnew v hv).trans
85       (mul_le_mul_of_nonneg_right (le_max_left α β) (norm_nonneg v))
86   have hm : 0 ≤ max α β := le_trans hα (le_max_left α β)
87   have hw2 := (sq_le_sq₀ (norm_nonneg w) (mul_nonneg hm (norm_nonneg u))).mpr hwu
88   have hz2 := (sq_le_sq₀ (norm_nonneg z) (mul_nonneg hm (norm_nonneg v))).mpr hzv
89   apply (sq_le_sq₀ (norm_nonneg _) (mul_nonneg hm (norm_nonneg x))).mp
90   rw [hsq,mul_pow,hxnorm]
91   rw [mul_pow] at hw2 hz2
92   nlinarith
93 
94 /-- Two residual certificates control motion without preserving the old kernel. -/
95 theorem projection_motion (B : ResidualRobustness.Bound d)
96     (B' : ResidualRobustness.Bound e) {ε : ℝ} (hε : 0 ≤ ε)
97     (he : ∀ x, ‖(d-e) x‖ ≤ ε*‖x‖) (x : E) :
98     ‖projection d x-projection e x‖ ≤ max B.constant B'.constant * ε * ‖x‖ := by
99   have hrev : ∀ z, ‖(e-d) z‖ ≤ ε*‖z‖ := by
100     intro z
101     simpa only [sub_apply, norm_sub_rev] using he z
102   have hb := projection_motion_of_directional d e
103     (mul_nonneg B.nonneg hε) (mul_nonneg B'.nonneg hε)
104     (fun z hz => B.new_exact_near_old e ε he z hz)
105     (fun z hz => B'.new_exact_near_old d ε hrev z hz) x
106   simpa only [max_mul_of_nonneg _ _ hε] using hb
107 
108 /-- The comparison is an operator-norm statement, not a sampled-vector claim. -/
109 theorem projection_opNorm (B : ResidualRobustness.Bound d)
110     (B' : ResidualRobustness.Bound e) {ε : ℝ} (he : ‖d-e‖ ≤ ε) :
111     ‖projection d-projection e‖ ≤ max B.constant B'.constant * ε := by
112   have hε : 0 ≤ ε := (norm_nonneg (d-e)).trans he
113   apply ContinuousLinearMap.opNorm_le_bound _ (mul_nonneg
114     (B.nonneg.trans (le_max_left _ _)) hε)
115   intro x
116   exact projection_motion d e B B' hε
117     (fun z => ((d-e).le_opNorm z).trans
118       (mul_le_mul_of_nonneg_right he (norm_nonneg z))) x
119 
120 /-- Errors in the candidate and in the model contribute separately. -/
121 theorem repaired_input_motion (B : ResidualRobustness.Bound d)
122     (B' : ResidualRobustness.Bound e) {ε : ℝ} (he : ‖d-e‖ ≤ ε) (x y : E) :
123     ‖projection d x-projection e y‖ ≤
124       ‖x-y‖ + (max B.constant B'.constant * ε)*‖y‖ := by
125   calc
126     _ ≤ ‖projection d x-projection d y‖ + ‖projection d y-projection e y‖ :=
127       norm_sub_le_norm_sub_add_norm_sub _ _ _
128     _ ≤ ‖x-y‖ + (max B.constant B'.constant * ε)*‖y‖ := by
129       apply add_le_add
130       · simpa only [map_sub] using projection_norm d (x-y)
131       · exact ((projection d-projection e).le_opNorm y).trans
132           (mul_le_mul_of_nonneg_right (projection_opNorm d e B B' he) (norm_nonneg y))
133 
134 /-- Distance-to-exactness also changes by at most the projection-motion budget. -/
135 theorem distance_motion (B : ResidualRobustness.Bound d)
136     (B' : ResidualRobustness.Bound e) {ε : ℝ} (he : ‖d-e‖ ≤ ε) (x : E) :
137     |‖x-projection d x‖-‖x-projection e x‖| ≤
138       (max B.constant B'.constant * ε)*‖x‖ := by
139   have h := abs_norm_sub_norm_le (x-projection d x) (x-projection e x)
140   have hid : (x-projection d x)-(x-projection e x)=projection e x-projection d x := by abel
141   rw [hid] at h
142   have hs : ‖projection e x-projection d x‖ = ‖projection d x-projection e x‖ := norm_sub_rev _ _
143   rw [hs] at h
144   exact h.trans (((projection d-projection e).le_opNorm x).trans
145     (mul_le_mul_of_nonneg_right (projection_opNorm d e B B' he) (norm_nonneg x)))
146 
147 /-- Losing a unit exact direction forces the new residual gain to blow up. -/
148 theorem lost_exact_unit_forces_gain (B' : ResidualRobustness.Bound e)
149     {ε : ℝ} (he : ‖d-e‖ ≤ ε) (x : E) (hx : d x=0)
150     (hn : ‖x‖=1) (hp : projection e x=0) : 1 ≤ B'.constant*ε := by
151   have hrev : ∀ z, ‖(e-d) z‖ ≤ ε*‖z‖ := by
152     intro z
153     have h := ((d-e).le_opNorm z).trans
154       (mul_le_mul_of_nonneg_right he (norm_nonneg z))
155     simpa only [sub_apply,norm_sub_rev] using h
156   have h := B'.new_exact_near_old d ε hrev x hx
157   simpa only [hp,sub_zero,hn,mul_one] using h
158 
159 /-- Models sharing one certified residual-gain bound. Their kernels may differ. -/
160 abbrev StableModel (M : NNReal) :=
161   {f : E →L[ℝ] R // ∀ x, ‖x-projection f x‖ ≤ (M:ℝ)*‖f x‖}
162 
163 /-- The projector is Lipschitz on each uniformly certified model class. -/
164 theorem projection_lipschitz (M : NNReal) :
165     LipschitzWith M (fun f : StableModel (E := E) (R := R) M => projection f.val) := by
166   apply LipschitzWith.of_dist_le_mul
167   intro f g
168   let B : ResidualRobustness.Bound f.val := ⟨M,M.property,f.property⟩
169   let B' : ResidualRobustness.Bound g.val := ⟨M,M.property,g.property⟩
170   have h := projection_opNorm f.val g.val B B' (le_refl ‖f.val-g.val‖)
171   simpa only [B,B',max_self,Subtype.dist_eq,dist_eq_norm] using h
172 
173 theorem continuous_projection (M : NNReal) :
174     Continuous (fun f : StableModel (E := E) (R := R) M => projection f.val) :=
175   (projection_lipschitz M).continuous
176 
177 end MovingKernel
178 end KomorebiSpace
179 end

Back to source controls