SurjectiveKernelMotion.lean

1 import KomorebiSpace.SplitKernelPerturbation
2 
3 set_option autoImplicit false
4 
5 /-!
6 # Constructing the splitting from a surjective Hilbert defect
7 
8 The right inverse required by SplitKernel is derived here from surjectivity and
9 the Hilbert orthogonal complement. A pre-existing residual bound controls its
10 norm. Consequently a perturbed bound and a moving-kernel equivalence need only
11 the old certificate, surjectivity, and a strict operator-error radius.
12 -/
13 universe u v
14 noncomputable section
15 namespace KomorebiSpace
16 namespace SurjectiveKernel
17 open HilbertKernelProjection
18 variable {E : Type u} {R : Type v}
19 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
20 variable [NormedAddCommGroup R] [NormedSpace ℝ R] [CompleteSpace R]
21 variable (d : E →L[ℝ] R) (hd : Function.Surjective d)
22 
23 include hd in
24 omit [CompleteSpace R] in
25 theorem reduced_surjective : Function.Surjective (reduced d) := by
26   intro r
27   obtain ⟨x,hx⟩ := hd r
28   refine ⟨⟨x-projection d x,error_orthogonal d x⟩,?_⟩
29   exact (defect_error d x).trans hx
30 
31 /-- Restriction to the orthogonal complement is a continuous linear equivalence. -/
32 def transverseEquiv : d.kerᗮ ≃L[ℝ] R :=
33   ContinuousLinearEquiv.ofBijective (reduced d)
34     (LinearMap.ker_eq_bot.mpr (reduced_injective d))
35     (LinearMap.range_eq_top.mpr (reduced_surjective d hd))
36 
37 /-- Canonical minimal-norm right inverse for the declared Hilbert geometry. -/
38 def sectionMap : R →L[ℝ] E :=
39   d.kerᗮ.subtypeL.comp (transverseEquiv d hd).symm.toContinuousLinearMap
40 
41 @[simp] theorem section_right (r : R) : d (sectionMap d hd r) = r :=
42   (transverseEquiv d hd).apply_symm_apply r
43 
44 theorem section_orthogonal (r : R) : sectionMap d hd r ∈ d.kerᗮ :=
45   ((transverseEquiv d hd).symm r).property
46 
47 theorem section_bound (B : ResidualRobustness.Bound d) (r : R) :
48     ‖sectionMap d hd r‖ ≤ B.constant*‖r‖ := by
49   have h := B.estimate (sectionMap d hd r)
50   rw [projection_orthogonal_zero d _ (section_orthogonal d hd r),sub_zero,section_right] at h
51   exact h
52 
53 /-- No right inverse or new-kernel stability is supplied in this interface. -/
54 def certificate (B : ResidualRobustness.Bound d) (e : E →L[ℝ] R)
55     {ε : ℝ} (hε : 0 ≤ ε) (he : ‖d-e‖ ≤ ε) (hs : B.constant*ε<1) :
56     SplitKernel.Certificate d e where
57   sectionMap := sectionMap d hd
58   right_inverse := section_right d hd
59   constant := B.constant
60   nonneg := B.nonneg
61   section_bound := section_bound d hd B
62   epsilon := ε
63   epsilon_nonneg := hε
64   operator_error := he
65   small := hs
66 
67 /-- Surjectivity persists and supplies a full perturbed residual bound. -/
68 def perturbedBound (B : ResidualRobustness.Bound d) (e : E →L[ℝ] R)
69     {ε : ℝ} (hε : 0 ≤ ε) (he : ‖d-e‖ ≤ ε) (hs : B.constant*ε<1) :
70     ResidualRobustness.Bound e := (certificate d hd B e hε he hs).perturbedBound
71 
72 include hd in
73 theorem projection_motion (B : ResidualRobustness.Bound d) (e : E →L[ℝ] R)
74     {ε : ℝ} (hε : 0 ≤ ε) (he : ‖d-e‖ ≤ ε) (hs : B.constant*ε<1) :
75     ‖projection d-projection e‖ ≤ (B.constant*ε)/(1-B.constant*ε) :=
76   (certificate d hd B e hε he hs).projection_motion
77 
78 /-- The perturbed exact space is explicitly equivalent, not asserted equal. -/
79 def kernelEquiv (B : ResidualRobustness.Bound d) (e : E →L[ℝ] R)
80     {ε : ℝ} (hε : 0 ≤ ε) (he : ‖d-e‖ ≤ ε) (hs : B.constant*ε<1) :
81     d.ker ≃L[ℝ] e.ker := (certificate d hd B e hε he hs).kernelEquiv
82 
83 end SurjectiveKernel
84 end KomorebiSpace
85 end

Back to source controls