KernelProjectionBounds.lean

1 import Mathlib.Analysis.InnerProductSpace.Projection.Basic
2 import Mathlib.Analysis.Normed.Module.FiniteDimension
3 import Mathlib.Tactic.Abel
4 import Mathlib.Tactic.Positivity
5 
6 set_option autoImplicit false
7 
8 /-!
9 # Finite-dimensional kernel correction with a derived sharp gain
10 
11 The correction is the orthogonal projection onto the actual kernel. The gain
12 is the norm of the inverse of the defect restricted to the orthogonal
13 complement. No lower bound, spectral gap, or right inverse is assumed.
14 The residual norm is the norm of the supplied target space; it need not be
15 an inner-product norm. These are classical finite-dimensional constructions,
16 not executable singular-value algorithms or uniform bounds over all maps.
17 -/
18 universe u v
19 noncomputable section
20 namespace KomorebiSpace
21 namespace KernelProjection
22 variable {E : Type u} {R : Type v}
23 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
24 variable [NormedAddCommGroup R] [NormedSpace ℝ R]
25 variable (d : E →L[ℝ] R)
26 
27 /-- Canonical for the specified inner product and the actual defect kernel. -/
28 def projection : E →L[ℝ] E := d.ker.starProjection
29 
30 @[simp] theorem projection_mem (x : E) : projection d x ∈ d.ker :=
31   d.ker.starProjection_apply_mem x
32 
33 @[simp] theorem projection_exact (x : E) : d (projection d x) = 0 :=
34   projection_mem d x
35 
36 @[simp] theorem projection_fixes (x : E) (hx : d x = 0) : projection d x = x :=
37   d.ker.starProjection_eq_self_iff.mpr hx
38 
39 @[simp] theorem projection_idempotent (x : E) :
40     projection d (projection d x) = projection d x :=
41   projection_fixes d _ (projection_exact d x)
42 
43 theorem projection_norm (x : E) : ‖projection d x‖ ≤ ‖x‖ :=
44   d.ker.norm_starProjection_apply_le x
45 
46 theorem projection_opNorm : ‖projection d‖ ≤ 1 := d.ker.starProjection_norm_le
47 
48 theorem error_orthogonal (x : E) : x - projection d x ∈ d.kerᗮ :=
49   d.ker.sub_starProjection_mem_orthogonal x
50 
51 @[simp] theorem defect_error (x : E) : d (x - projection d x) = d x := by
52   rw [map_sub, projection_exact, sub_zero]
53 
54 theorem projection_orthogonal_zero (x : E) (hx : x ∈ d.kerᗮ) :
55     projection d x = 0 := by
56   change d.ker.starProjection x = 0
57   exact d.ker.starProjection_apply_eq_zero_iff.mpr hx
58 
59 /-- The residual map on the complementary directions has no kernel. -/
60 def reduced : d.kerᗮ →L[ℝ] R := d.comp d.kerᗮ.subtypeL
61 
62 omit [FiniteDimensional ℝ E] in
63 @[simp] theorem reduced_apply (x : d.kerᗮ) : reduced d x = d x.val := rfl
64 
65 omit [FiniteDimensional ℝ E] in
66 theorem reduced_injective : Function.Injective (reduced d) := by
67   intro x y h
68   apply Subtype.ext
69   apply sub_eq_zero.mp
70   have hk : x.val - y.val ∈ d.ker := by
71     change d (x.val - y.val) = 0
72     rw [map_sub]
73     exact sub_eq_zero.mpr h
74   have ho : x.val - y.val ∈ d.kerᗮ := d.kerᗮ.sub_mem x.property y.property
75   exact inner_self_eq_zero.mp (ho _ hk)
76 
77 /-- Finite dimensionality supplies continuity of this inverse on the actual range. -/
78 def reducedEquiv : d.kerᗮ ≃L[ℝ] LinearMap.range (reduced d).toLinearMap :=
79   (LinearEquiv.ofInjective (reduced d).toLinearMap (reduced_injective d)).toContinuousLinearEquiv
80 
81 @[simp] theorem reducedEquiv_value (x : d.kerᗮ) :
82     (reducedEquiv d x).val = d x.val := rfl
83 
84 /-- Sharp residual-to-kernel-distance gain for the supplied norms. It is zero
85 when the complementary space is zero; no undefined least-positive singular
86 value is used in that case. -/
87 def gain : ℝ := ‖(reducedEquiv d).symm.toContinuousLinearMap‖
88 
89 theorem gain_nonneg : 0 ≤ gain d := by
90   unfold gain
91   exact norm_nonneg ((reducedEquiv d).symm.toContinuousLinearMap)
92 
93 theorem complement_bound (x : d.kerᗮ) : ‖x.val‖ ≤ gain d * ‖d x.val‖ := by
94   have hb := (reducedEquiv d).symm.toContinuousLinearMap.le_opNorm (reducedEquiv d x)
95   change ‖(reducedEquiv d).symm (reducedEquiv d x)‖ ≤ gain d * ‖d x.val‖ at hb
96   simpa only [ContinuousLinearEquiv.symm_apply_apply, Submodule.norm_coe] using hb
97 
98 
99 /-- The formerly assumed correction estimate is derived. -/
100 theorem error_bound (x : E) : ‖x - projection d x‖ ≤ gain d * ‖d x‖ := by
101   have hb := complement_bound d ⟨x - projection d x, error_orthogonal d x⟩
102   simpa only [defect_error] using hb
103 
104 /-- Orthogonal correction minimizes anchor displacement, not necessarily a
105 separate global product norm after graph reconstruction. -/
106 theorem projection_best (x y : E) (hy : d y = 0) :
107     ‖x - projection d x‖ ≤ ‖x - y‖ := by
108   calc
109     _ = ‖(x-y) - projection d (x-y)‖ := by
110       rw [map_sub, projection_fixes d y hy]
111       congr 1
112       abel
113     _ = ‖d.kerᗮ.starProjection (x-y)‖ := by
114       rw [Submodule.starProjection_orthogonal_val]
115       rfl
116     _ ≤ _ := d.kerᗮ.norm_starProjection_apply_le (x-y)
117 
118 /-- Characterization by the protected kernel and orthogonal displacement. -/
119 theorem projection_unique (x y : E) (hy : d y = 0)
120     (ho : x-y ∈ d.kerᗮ) : projection d x = y :=
121   d.ker.eq_starProjection_of_mem_orthogonal hy ho
122 
123 /-- Only the kernel, rather than its presentation by a defect map, determines the projection. -/
124 theorem projection_eq_of_kernel_eq (e : E →L[ℝ] R) (h : d.ker = e.ker) :
125     projection d = projection e := by
126   ext x
127   apply projection_unique d x (projection e x)
128   · change projection e x ∈ d.ker
129     rw [h]
130     exact projection_mem e x
131   · rw [h]
132     exact error_orthogonal e x
133 
134 /-- No smaller nonnegative constant works for all inputs with these norms. -/
135 theorem gain_le_of_bound (C : ℝ) (hC : 0 ≤ C)
136     (hb : ∀ x, ‖x-projection d x‖ ≤ C * ‖d x‖) : gain d ≤ C := by
137   apply ContinuousLinearMap.opNorm_le_bound _ hC
138   intro r
139   let x := (reducedEquiv d).symm r
140   have hx := hb x.val
141   rw [projection_orthogonal_zero d x.val x.property, sub_zero] at hx
142   have hd : d x.val = r.val := by
143     have he := congrArg Subtype.val ((reducedEquiv d).apply_symm_apply r)
144     exact he
145   simpa only [hd, Submodule.norm_coe, x, ContinuousLinearEquiv.coe_coe] using hx
146 
147 theorem gain_characterization (C : ℝ) (hC : 0 ≤ C) :
148     (∀ x, ‖x-projection d x‖ ≤ C * ‖d x‖) ↔ gain d ≤ C := by
149   constructor
150   · exact gain_le_of_bound d C hC
151   · intro h x
152     exact (error_bound d x).trans (mul_le_mul_of_nonneg_right h (norm_nonneg _))
153 
154 /-- The degenerate all-exact case has zero gain, rather than an undefined singular value. -/
155 theorem gain_eq_zero_iff : gain d = 0 ↔ d = 0 := by
156   constructor
157   · intro hg
158     ext x
159     have hb := error_bound d x
160     rw [hg,zero_mul] at hb
161     have hx : x-projection d x=0 := norm_eq_zero.mp (le_antisymm hb (norm_nonneg _))
162     have he : x=projection d x := sub_eq_zero.mp hx
163     change d x=0
164     rw [he]
165     exact projection_exact d x
166   · intro hd
167     apply le_antisymm _ (gain_nonneg d)
168     apply gain_le_of_bound d 0 le_rfl
169     intro x
170     have hx : d x=0 := by rw [hd]; rfl
171     rw [projection_fixes d x hx,sub_self,norm_zero,zero_mul]
172 
173 theorem stable_kernel_projection :
174     ∃ C : ℝ, 0 ≤ C ∧ ∀ x, d (projection d x) = 0 ∧
175       ‖x-projection d x‖ ≤ C * ‖d x‖ :=
176   ⟨gain d, gain_nonneg d, fun x => ⟨projection_exact d x, error_bound d x⟩⟩
177 
178 end KernelProjection
179 end KomorebiSpace
180 end

Back to source controls