MovingKernelExamples.lean

1 import KomorebiSpace.SurjectiveKernelMotion
2 import KomorebiSpace.MovingDescent
3 import KomorebiSpace.EuclideanCertificateCoordinates
4 import Mathlib.Tactic.FieldSimp
5 import Mathlib.Tactic.NormNum
6 
7 set_option autoImplicit false
8 
9 /-!
10 # An exactly moving kernel, its projector, and the strict-radius boundary
11 
12 The Euclidean two-dimensional defect is d_t(x,y)=x+t*y. Its kernel is the moving
13 line (-t*b,b), not the old vertical axis. The projection and its full operator
14 motion are computed exactly for every real t. The general split perturbation
15 and two-stage-descent interfaces are instantiated, not only a separate formula.
16 -/
17 noncomputable section
18 namespace KomorebiSpace
19 namespace MovingKernelExamples
20 open HilbertKernelProjection
21 abbrev H := ExactCoordinates.Space 2
22 
23 def vec (a b : ℝ) : H := WithLp.toLp 2 ![a,b]
24 
25 theorem norm_sq (x : H) : ‖x‖^2=(x 0)^2+(x 1)^2 := by
26   simpa only [Fin.sum_univ_two] using ExactCoordinates.norm_squared 2 x
27 
28 def defectLinear (t : ℝ) : H →ₗ[ℝ] ℝ where
29   toFun x := x 0+t*x 1
30   map_add' x y := by simp only [PiLp.add_apply]; ring
31   map_smul' a x := by
32     change a*x 0+t*(a*x 1)=a*(x 0+t*x 1)
33     ring
34 
35 def defect (t : ℝ) : H →L[ℝ] ℝ := (defectLinear t).toContinuousLinearMap
36 @[simp] theorem defect_apply (t : ℝ) (x : H) : defect t x=x 0+t*x 1 := rfl
37 
38 def sectionLinear : ℝ →ₗ[ℝ] H where
39   toFun r := vec r 0
40   map_add' x y := by ext i; fin_cases i <;> simp [vec,PiLp.add_apply]
41   map_smul' a x := by ext i; fin_cases i <;> simp [vec,PiLp.smul_apply]
42 
43 def sectionMap : ℝ →L[ℝ] H := sectionLinear.toContinuousLinearMap
44 @[simp] theorem section_apply (r : ℝ) : sectionMap r=vec r 0 := rfl
45 
46 theorem section_norm (r : ℝ) : ‖sectionMap r‖=‖r‖ := by
47   apply (sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)).mp
48   rw [norm_sq,Real.norm_eq_abs,sq_abs]
49   simp [section_apply,vec]
50 
51 @[simp] theorem section_right (t r : ℝ) : defect t (sectionMap r)=r := by
52   simp [defect_apply,section_apply,vec]
53 
54 def selfCertificate (t : ℝ) : SplitKernel.Certificate (defect t) (defect t) where
55   sectionMap := sectionMap
56   right_inverse := section_right t
57   constant := 1
58   nonneg := by norm_num
59   section_bound r := by rw [section_norm,one_mul]
60   epsilon := 0
61   epsilon_nonneg := le_rfl
62   operator_error := by simp
63   small := by norm_num
64 
65 /-- Both systems have gain at most one, uniformly over all real slopes. -/
66 def bound (t : ℝ) : ResidualRobustness.Bound (defect t) :=
67   (selfCertificate t).referenceBound
68 
69 @[simp] theorem bound_constant (t : ℝ) : (bound t).constant=1 := rfl
70 
71 theorem defect_surjective (t : ℝ) : Function.Surjective (defect t) :=
72   fun r => ⟨sectionMap r,section_right t r⟩
73 
74 theorem kernel_parameter (t : ℝ) (x : H) :
75     defect t x=0 ↔ x=vec (-t*x 1) (x 1) := by
76   constructor
77   · intro h
78     have h0 : x 0 = -t*x 1 := by change x 0+t*x 1=0 at h; linarith
79     ext i
80     fin_cases i <;> simp [vec,h0]
81   · intro h
82     rw [h]
83     simp [defect_apply,vec]
84 
85 def projected (t : ℝ) (x : H) : H :=
86   vec (-t*((x 1-t*x 0)/(1+t^2))) ((x 1-t*x 0)/(1+t^2))
87 
88 theorem projected_exact (t : ℝ) (x : H) : defect t (projected t x)=0 := by
89   simp [projected,defect_apply,vec]
90 
91 theorem projection_formula (t : ℝ) (x : H) : projection (defect t) x=projected t x := by
92   apply projection_unique
93   · exact projected_exact t x
94   · intro y hy
95     have hy0 : y 0 = -t*y 1 := by change y 0+t*y 1=0 at hy; linarith
96     rw [ExactCoordinates.inner_coordinates,Fin.sum_univ_two]
97     simp only [PiLp.sub_apply,projected,vec,Matrix.cons_val_zero,
98       Matrix.cons_val_one,hy0]
99     have ht : (1+t^2:ℝ) ≠ 0 := by positivity
100     field_simp
101     ring
102 
103 @[simp] theorem zero_projection (x : H) : projection (defect 0) x=vec 0 (x 1) := by
104   rw [projection_formula]
105   simp [projected]
106 
107 /-- Norm closeness is a theorem about operators, not a list of test vectors. -/
108 theorem defect_distance (s t : ℝ) : ‖defect s-defect t‖ ≤ |s-t| := by
109   apply ContinuousLinearMap.opNorm_le_bound _ (abs_nonneg _)
110   intro x
111   have hid : (defect s-defect t) x=(s-t)*x 1 := by simp only [sub_apply,defect_apply]; ring
112   rw [hid,norm_mul,Real.norm_eq_abs,Real.norm_eq_abs]
113   apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)
114   apply (sq_le_sq₀ (abs_nonneg _) (norm_nonneg _)).mp
115   rw [sq_abs,norm_sq]
116   nlinarith [sq_nonneg (x 0)]
117 
118 /-- The generic two-sided theorem is instantiated for the actual moving line. -/
119 theorem generic_motion (s t : ℝ) :
120     ‖projection (defect s)-projection (defect t)‖ ≤ |s-t| := by
121   have h := MovingKernel.projection_opNorm _ _ (bound s) (bound t) (defect_distance s t)
122   simpa only [bound_constant,max_self,one_mul] using h
123 
124 /-- Exact squared pointwise motion relative to the vertical-axis reference. -/
125 theorem motion_squared (t : ℝ) (x : H) :
126     ‖projection (defect t) x-projection (defect 0) x‖^2 =
127       (t^2/(1+t^2))*‖x‖^2 := by
128   rw [projection_formula,zero_projection,norm_sq,norm_sq]
129   simp only [PiLp.sub_apply,projected,vec,Matrix.cons_val_zero,
130     Matrix.cons_val_one]
131   have ht : (1+t^2:ℝ) ≠ 0 := by positivity
132   field_simp
133   ring
134 
135 theorem motion_formula (t : ℝ) (x : H) :
136     ‖projection (defect t) x-projection (defect 0) x‖ =
137       Real.sqrt (t^2/(1+t^2))*‖x‖ := by
138   apply (sq_eq_sq₀ (norm_nonneg _) (mul_nonneg (Real.sqrt_nonneg _) (norm_nonneg _))).mp
139   rw [motion_squared,mul_pow,Real.sq_sqrt (by positivity)]
140 
141 /-- The complete operator norm is calculated, not just bounded. -/
142 theorem motion_opNorm_exact (t : ℝ) :
143     ‖projection (defect t)-projection (defect 0)‖ = Real.sqrt (t^2/(1+t^2)) := by
144   apply le_antisymm
145   · apply ContinuousLinearMap.opNorm_le_bound _ (Real.sqrt_nonneg _)
146     intro x
147     exact (motion_formula t x).le
148   · have h := (projection (defect t)-projection (defect 0)).le_opNorm (vec 1 0)
149     have hn : ‖vec 1 0‖=1 := by
150       have h := section_norm 1
151       simpa only [section_apply,norm_one] using h
152     change ‖projection (defect t) (vec 1 0)-projection (defect 0) (vec 1 0)‖ ≤ _ at h
153     rw [motion_formula,hn,mul_one,mul_one] at h
154     exact h
155 
156 /-- The old nonzero exact vector generally stops being exact, while a new one exists. -/
157 theorem exact_space_really_moves (t : ℝ) (ht : t ≠ 0) :
158     defect 0 (vec 0 7)=0 ∧ defect t (vec 0 7)≠0 ∧
159       defect t (vec (-7*t) 7)=0 ∧ vec (-7*t) 7 ≠ 0 := by
160   constructor
161   · norm_num [defect_apply,vec]
162   constructor
163   · simpa [defect_apply,vec] using ht
164   constructor
165   · simp [defect_apply,vec]; ring
166   · intro h
167     have h1 := congrArg (fun x : H => x 1) h
168     norm_num [vec] at h1
169 
170 /-- The small-radius perturbation construction is fully discharged on an interval. -/
171 def intervalCertificate (t : ℝ) (ht : |t|<1) : SplitKernel.Certificate (defect 0) (defect t) where
172   sectionMap := sectionMap
173   right_inverse := section_right 0
174   constant := 1
175   nonneg := by norm_num
176   section_bound r := by rw [section_norm,one_mul]
177   epsilon := |t|
178   epsilon_nonneg := abs_nonneg t
179   operator_error := by simpa only [zero_sub,abs_neg] using defect_distance 0 t
180   small := by simpa only [one_mul] using ht
181 
182 theorem interval_residual_identity (t : ℝ) (ht : |t|<1) (r : ℝ) :
183     (intervalCertificate t ht).residualEquiv r=r := by
184   rw [SplitKernel.Certificate.residualEquiv_apply]
185   exact section_right t r
186 
187 theorem interval_inverse_identity (t : ℝ) (ht : |t|<1) (r : ℝ) :
188     (intervalCertificate t ht).residualEquiv.symm r=r := by
189   have h := (intervalCertificate t ht).residualEquiv.apply_symm_apply r
190   rw [interval_residual_identity] at h
191   exact h
192 
193 theorem interval_section_identity (t : ℝ) (ht : |t|<1) (r : ℝ) :
194     (intervalCertificate t ht).perturbedSection r=sectionMap r := by
195   change sectionMap ((intervalCertificate t ht).residualEquiv.symm r)=_
196   rw [interval_inverse_identity]
197 
198 /-- The actual general kernel equivalence preserves the second coordinate. -/
199 theorem kernel_transport_formula (t : ℝ) (ht : |t|<1) (b : ℝ) :
200     ((intervalCertificate t ht).kernelEquiv
201       ⟨vec 0 b,by simp [defect_apply,vec]⟩).val=vec (-t*b) b := by
202   change vec 0 b-(intervalCertificate t ht).perturbedSection (defect t (vec 0 b))=_
203   rw [interval_section_identity,section_apply]
204   ext i
205   fin_cases i <;> simp [vec,defect_apply,PiLp.sub_apply]
206 
207 /-- The unchanged two-stage descent repair specializes to this moving projector. -/
208 theorem descent_repair_agreement (t : ℝ) (x : H) :
209     QuantitativeDescent.repair (0 : H →L[ℝ] ℝ) (defect t) x=projection (defect t) x := by
210   rw [QuantitativeDescent.repair_eq_projection]
211   apply projection_unique
212   · exact (QuantitativeDescent.joint_zero_iff _ _ _).mpr
213       ⟨by simp,projection_exact (defect t) x⟩
214   · intro y hy
215     exact error_orthogonal (defect t) x y
216       ((QuantitativeDescent.joint_zero_iff _ _ y).mp hy).2
217 
218 /-- The exact comparison formula now concerns an actual v0.30 descent output. -/
219 theorem descent_motion_squared (t : ℝ) (x : H) :
220     ‖QuantitativeDescent.repair (0 : H →L[ℝ] ℝ) (defect t) x-
221       QuantitativeDescent.repair (0 : H →L[ℝ] ℝ) (defect 0) x‖^2=
222       (t^2/(1+t^2))*‖x‖^2 := by
223   rw [descent_repair_agreement,descent_repair_agreement]
224   exact motion_squared t x
225 
226 /-- At radius one a surjective defect may become the zero map. Strictness matters. -/
227 theorem closed_radius_failure :
228     ‖(ContinuousLinearMap.id ℝ ℝ)-(0 : ℝ →L[ℝ] ℝ)‖ ≤ 1 ∧
229     ¬ Function.Surjective (0 : ℝ →L[ℝ] ℝ) := by
230   constructor
231   · simpa only [sub_zero] using ContinuousLinearMap.norm_id_le (𝕜 := ℝ) (E := ℝ)
232   · intro h
233     obtain ⟨x,hx⟩ := h 1
234     norm_num at hx
235 
236 end MovingKernelExamples
237 end KomorebiSpace
238 end

Back to source controls