HilbertKernelProjection.lean

1 import Mathlib.Analysis.InnerProductSpace.Projection.Basic
2 import Mathlib.Analysis.Normed.Operator.Banach
3 import KomorebiSpace.KernelProjectionBounds
4 import Mathlib.Tactic.Abel
5 import Mathlib.Tactic.Positivity
6 
7 set_option autoImplicit false
8 
9 /-!
10 # Hilbert kernel projection: exact repair versus residual stability
11 
12 The orthogonal repair exists for every bounded linear map from a real Hilbert
13 space. A finite residual-to-distance gain is equivalent to closed range when
14 the target is Banach. The inverse is constructed by the Banach open mapping
15 theorem, not an assumed bounded inverse. No finite dimensionality is required.
16 -/
17 universe u v
18 noncomputable section
19 namespace KomorebiSpace
20 namespace HilbertKernelProjection
21 variable {E : Type u} {R : Type v}
22 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
23 variable [NormedAddCommGroup R] [NormedSpace ℝ R]
24 variable (d : E →L[ℝ] R)
25 
26 /-- Canonical for the specified inner product and the actual defect kernel. -/
27 def projection : E →L[ℝ] E := d.ker.starProjection
28 
29 @[simp] theorem projection_mem (x : E) : projection d x ∈ d.ker :=
30   d.ker.starProjection_apply_mem x
31 
32 @[simp] theorem projection_exact (x : E) : d (projection d x) = 0 :=
33   projection_mem d x
34 
35 @[simp] theorem projection_fixes (x : E) (hx : d x = 0) : projection d x = x :=
36   d.ker.starProjection_eq_self_iff.mpr hx
37 
38 @[simp] theorem projection_idempotent (x : E) :
39     projection d (projection d x) = projection d x :=
40   projection_fixes d _ (projection_exact d x)
41 
42 theorem projection_norm (x : E) : ‖projection d x‖ ≤ ‖x‖ :=
43   d.ker.norm_starProjection_apply_le x
44 
45 theorem projection_opNorm : ‖projection d‖ ≤ 1 := d.ker.starProjection_norm_le
46 
47 theorem error_orthogonal (x : E) : x - projection d x ∈ d.kerᗮ :=
48   d.ker.sub_starProjection_mem_orthogonal x
49 
50 @[simp] theorem defect_error (x : E) : d (x - projection d x) = d x := by
51   rw [map_sub, projection_exact, sub_zero]
52 
53 theorem projection_orthogonal_zero (x : E) (hx : x ∈ d.kerᗮ) :
54     projection d x = 0 := by
55   change d.ker.starProjection x = 0
56   exact d.ker.starProjection_apply_eq_zero_iff.mpr hx
57 
58 /-- The residual map on the complementary directions has no kernel. -/
59 def reduced : d.kerᗮ →L[ℝ] R := d.comp d.kerᗮ.subtypeL
60 
61 omit [CompleteSpace E] in
62 @[simp] theorem reduced_apply (x : d.kerᗮ) : reduced d x = d x.val := rfl
63 
64 omit [CompleteSpace E] in
65 theorem reduced_injective : Function.Injective (reduced d) := by
66   intro x y h
67   apply Subtype.ext
68   apply sub_eq_zero.mp
69   have hk : x.val - y.val ∈ d.ker := by
70     change d (x.val - y.val) = 0
71     rw [map_sub]
72     exact sub_eq_zero.mpr h
73   have ho : x.val - y.val ∈ d.kerᗮ := d.kerᗮ.sub_mem x.property y.property
74   exact inner_self_eq_zero.mp (ho _ hk)
75 
76 /-- Projection removes only kernel components, so the reduced range is the full range. -/
77 theorem reduced_range : Set.range (reduced d) = Set.range d := by
78   ext y
79   constructor
80   · rintro ⟨x, rfl⟩
81     exact ⟨x.val, rfl⟩
82   · rintro ⟨x, rfl⟩
83     exact ⟨⟨x - projection d x, error_orthogonal d x⟩, defect_error d x⟩
84 
85 variable [CompleteSpace R]
86 
87 /-- Banach's inverse theorem supplies the inverse when the actual range is closed. -/
88 def reducedEquiv (hd : IsClosed (Set.range d)) :
89     d.kerᗮ ≃L[ℝ] LinearMap.range (reduced d).toLinearMap :=
90   (reduced d).equivRange (reduced_injective d) (by rw [reduced_range]; exact hd)
91 
92 variable (hd : IsClosed (Set.range d))
93 
94 @[simp] theorem reducedEquiv_value (x : d.kerᗮ) :
95     (reducedEquiv d hd x).val = d x.val := rfl
96 
97 /-- Sharp residual-to-kernel-distance gain for the supplied norms. It is zero
98 when the complementary space is zero; no undefined least-positive singular
99 value is used in that case. -/
100 def gain : ℝ := ‖(reducedEquiv d hd).symm.toContinuousLinearMap‖
101 
102 theorem gain_nonneg : 0 ≤ gain d hd := by
103   unfold gain
104   exact norm_nonneg ((reducedEquiv d hd).symm.toContinuousLinearMap)
105 
106 theorem complement_bound (x : d.kerᗮ) : ‖x.val‖ ≤ gain d hd * ‖d x.val‖ := by
107   have hb := (reducedEquiv d hd).symm.toContinuousLinearMap.le_opNorm (reducedEquiv d hd x)
108   change ‖(reducedEquiv d hd).symm (reducedEquiv d hd x)‖ ≤ gain d hd * ‖d x.val‖ at hb
109   simpa only [ContinuousLinearEquiv.symm_apply_apply, Submodule.norm_coe] using hb
110 
111 
112 /-- The formerly assumed correction estimate is derived. -/
113 theorem error_bound (x : E) : ‖x - projection d x‖ ≤ gain d hd * ‖d x‖ := by
114   have hb := complement_bound d hd ⟨x - projection d x, error_orthogonal d x⟩
115   simpa only [defect_error] using hb
116 
117 omit [CompleteSpace R] in
118 /-- Orthogonal correction minimizes anchor displacement, not necessarily a
119 separate global product norm after graph reconstruction. -/
120 theorem projection_best (x y : E) (hy : d y = 0) :
121     ‖x - projection d x‖ ≤ ‖x - y‖ := by
122   calc
123     _ = ‖(x-y) - projection d (x-y)‖ := by
124       rw [map_sub, projection_fixes d y hy]
125       congr 1
126       abel
127     _ = ‖d.kerᗮ.starProjection (x-y)‖ := by
128       rw [Submodule.starProjection_orthogonal_val]
129       rfl
130     _ ≤ _ := d.kerᗮ.norm_starProjection_apply_le (x-y)
131 
132 omit [CompleteSpace R] in
133 /-- Characterization by the protected kernel and orthogonal displacement. -/
134 theorem projection_unique (x y : E) (hy : d y = 0)
135     (ho : x-y ∈ d.kerᗮ) : projection d x = y :=
136   d.ker.eq_starProjection_of_mem_orthogonal hy ho
137 
138 omit [CompleteSpace R] in
139 /-- Only the kernel, rather than its presentation by a defect map, determines the projection. -/
140 theorem projection_eq_of_kernel_eq (e : E →L[ℝ] R) (h : d.ker = e.ker) :
141     projection d = projection e := by
142   ext x
143   apply projection_unique d x (projection e x)
144   · change projection e x ∈ d.ker
145     rw [h]
146     exact projection_mem e x
147   · rw [h]
148     exact error_orthogonal e x
149 
150 /-- No smaller nonnegative constant works for all inputs with these norms. -/
151 theorem gain_le_of_bound (C : ℝ) (hC : 0 ≤ C)
152     (hb : ∀ x, ‖x-projection d x‖ ≤ C * ‖d x‖) : gain d hd ≤ C := by
153   apply ContinuousLinearMap.opNorm_le_bound _ hC
154   intro r
155   let x := (reducedEquiv d hd).symm r
156   have hx := hb x.val
157   rw [projection_orthogonal_zero d x.val x.property, sub_zero] at hx
158   have hd : d x.val = r.val := by
159     have he := congrArg Subtype.val ((reducedEquiv d hd).apply_symm_apply r)
160     exact he
161   simpa only [hd, Submodule.norm_coe, x, ContinuousLinearEquiv.coe_coe] using hx
162 
163 theorem gain_characterization (C : ℝ) (hC : 0 ≤ C) :
164     (∀ x, ‖x-projection d x‖ ≤ C * ‖d x‖) ↔ gain d hd ≤ C := by
165   constructor
166   · exact gain_le_of_bound d hd C hC
167   · intro h x
168     exact (error_bound d hd x).trans (mul_le_mul_of_nonneg_right h (norm_nonneg _))
169 
170 /-- The degenerate all-exact case has zero gain, rather than an undefined singular value. -/
171 theorem gain_eq_zero_iff : gain d hd = 0 ↔ d = 0 := by
172   constructor
173   · intro hg
174     ext x
175     have hb := error_bound d hd x
176     rw [hg,zero_mul] at hb
177     have hx : x-projection d x=0 := norm_eq_zero.mp (le_antisymm hb (norm_nonneg _))
178     have he : x=projection d x := sub_eq_zero.mp hx
179     change d x=0
180     rw [he]
181     exact projection_exact d x
182   · intro hz
183     apply le_antisymm _ (gain_nonneg d hd)
184     apply gain_le_of_bound d hd 0 le_rfl
185     intro x
186     have hx : d x=0 := by rw [hz]; rfl
187     rw [projection_fixes d x hx,sub_self,norm_zero,zero_mul]
188 
189 theorem stable_kernel_projection (hd : IsClosed (Set.range d)) :
190     ∃ C : ℝ, 0 ≤ C ∧ ∀ x, d (projection d x) = 0 ∧
191       ‖x-projection d x‖ ≤ C * ‖d x‖ :=
192   ⟨gain d hd, gain_nonneg d hd, fun x => ⟨projection_exact d x, error_bound d hd x⟩⟩
193 
194 omit [CompleteSpace R] in
195 /-- A global residual-to-distance estimate forces closed range. -/
196 theorem closed_range_of_bound (C : ℝ) (hC : 0 ≤ C)
197     (hb : ∀ x, ‖x - projection d x‖ ≤ C * ‖d x‖) : IsClosed (Set.range d) := by
198   have ha : AntilipschitzWith ⟨C, hC⟩ (reduced d) := by
199     apply AntilipschitzWith.of_le_mul_dist
200     intro x y
201     rw [dist_eq_norm, dist_eq_norm, ← map_sub]
202     change ‖(x-y).val‖ ≤ C * ‖d (x-y).val‖
203     have h := hb (x-y).val
204     rw [projection_orthogonal_zero d _ (x-y).property, sub_zero] at h
205     exact h
206   have h := ha.isClosed_range (reduced d).uniformContinuous
207   rwa [reduced_range] at h
208 
209 /-- The exact infinite-dimensional criterion: stability iff closed range. -/
210 theorem closed_range_iff_bound : IsClosed (Set.range d) ↔
211     ∃ C : ℝ, 0 ≤ C ∧ ∀ x, ‖x - projection d x‖ ≤ C * ‖d x‖ := by
212   constructor
213   · intro h
214     exact ⟨gain d h, gain_nonneg d h, error_bound d h⟩
215   · rintro ⟨C, hC, hb⟩
216     exact closed_range_of_bound d C hC hb
217 
218 /-- No nonlinear choice of exact answers can bypass failure of the same bound. -/
219 theorem closed_range_iff_near_exact : IsClosed (Set.range d) ↔
220     ∃ C : ℝ, 0 ≤ C ∧ ∀ x : E, ∃ y : E,
221       d y = 0 ∧ ‖x-y‖ ≤ C * ‖d x‖ := by
222   constructor
223   · intro h
224     exact ⟨gain d h, gain_nonneg d h, fun x =>
225       ⟨projection d x, projection_exact d x, error_bound d h x⟩⟩
226   · rintro ⟨C,hC,hb⟩
227     apply closed_range_of_bound d C hC
228     intro x
229     obtain ⟨y,hy,he⟩ := hb x
230     exact (projection_best d x y hy).trans he
231 
232 /-- Unit vectors with arbitrarily small residual exclude closed range. -/
233 theorem not_closed_range_of_unit_witnesses
234     (hw : ∀ C : ℝ, 0 ≤ C → ∃ u : E,
235       u ∈ d.kerᗮ ∧ ‖u‖ = 1 ∧ C * ‖d u‖ < 1) :
236     ¬ IsClosed (Set.range d) := by
237   intro h
238   obtain ⟨u, hu, hn, hs⟩ := hw (gain d h) (gain_nonneg d h)
239   have hb := error_bound d h u
240   rw [projection_orthogonal_zero d u hu, sub_zero, hn] at hb
241   exact (not_lt_of_ge hb) hs
242 
243 omit [CompleteSpace R] in
244 /-- Exact repair exists irrespective of the closed-range condition. -/
245 theorem unconditional_exact_repair (x : E) :
246     d (projection d x) = 0 ∧ ‖projection d x‖ ≤ ‖x‖ :=
247   ⟨projection_exact d x, projection_norm d x⟩
248 
249 end HilbertKernelProjection
250 end KomorebiSpace
251 end

Back to source controls