ProtectedHilbertRepair.lean

1 import KomorebiSpace.HilbertKernelProjection
2 import Mathlib.Tactic.Linarith
3 
4 set_option autoImplicit false
5 
6 /-!
7 # KS56: nearest feasible repair preserving a declared continuous observable
8 
9 All corrections lie in the actual kernel of p. The closed-range condition is
10 on D restricted to that kernel, not on D alone. Feasibility is never assumed
11 for every raw vector. No closed-range hypothesis is used for nearest-point
12 existence or the Pythagorean identity.
13 -/
14 universe u v w
15 noncomputable section
16 namespace KomorebiSpace.ProtectedHilbertRepair
17 open scoped RealInnerProductSpace
18 variable {E : Type u} {R : Type v} {S : Type w}
19 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
20 variable [NormedAddCommGroup R] [NormedSpace ℝ R]
21 variable [NormedAddCommGroup S] [NormedSpace ℝ S]
22 variable (D : E →L[ℝ] R) (p : E →L[ℝ] S)
23 
24 /-- The actual admissible-correction operator on the protected kernel. -/
25 def restricted : p.ker →L[ℝ] R := D.comp p.ker.subtypeL
26 
27 omit [CompleteSpace E] in
28 @[simp] theorem restricted_apply (h : p.ker) : restricted D p h = D h.val := rfl
29 
30 def Feasible (x : E) : Prop := ∃ h : p.ker, restricted D p h = D x
31 
32 omit [CompleteSpace E] in
33 theorem feasible_iff_answer (x : E) :
34     Feasible D p x ↔ ∃ y : E, D y = 0 ∧ p y = p x := by
35   constructor
36   · rintro ⟨h, hh⟩
37     refine ⟨x-h.val, ?_, ?_⟩
38     · rw [map_sub]; exact sub_eq_zero.mpr hh.symm
39     · have hz : p h.val = 0 := h.property
40       rw [map_sub, hz, sub_zero]
41   · rintro ⟨y, hd, hp⟩
42     refine ⟨⟨x-y, ?_⟩, ?_⟩
43     · change p (x-y) = 0
44       rw [map_sub, hp, sub_self]
45     · change D (x-y) = D x
46       rw [map_sub, hd, sub_zero]
47 
48 def rawCorrection (x : E) (hx : Feasible D p x) : p.ker := Classical.choose hx
49 
50 omit [CompleteSpace E] in
51 theorem rawCorrection_image (x : E) (hx : Feasible D p x) :
52     restricted D p (rawCorrection D p x hx) = D x := Classical.choose_spec hx
53 
54 /-- Orthogonal displacement inside the protected kernel, not in the whole raw space. -/
55 def leastCorrection (x : E) (hx : Feasible D p x) : p.ker :=
56   rawCorrection D p x hx - HilbertKernelProjection.projection (restricted D p)
57     (rawCorrection D p x hx)
58 
59 theorem leastCorrection_image (x : E) (hx : Feasible D p x) :
60     restricted D p (leastCorrection D p x hx) = D x := by
61   rw [leastCorrection, HilbertKernelProjection.defect_error, rawCorrection_image]
62 
63 theorem leastCorrection_orthogonal (x : E) (hx : Feasible D p x) :
64     leastCorrection D p x hx ∈ (restricted D p).kerᗮ :=
65   HilbertKernelProjection.error_orthogonal _ _
66 
67 theorem leastCorrection_unique (x : E) (hx : Feasible D p x) (h : p.ker)
68     (hh : restricted D p h = D x) (ho : h ∈ (restricted D p).kerᗮ) :
69     h = leastCorrection D p x hx := by
70   have he : (⟨h, ho⟩ : (restricted D p).kerᗮ) =
71       ⟨leastCorrection D p x hx, leastCorrection_orthogonal D p x hx⟩ := by
72     apply HilbertKernelProjection.reduced_injective
73     change restricted D p h = restricted D p (leastCorrection D p x hx)
74     rw [hh, leastCorrection_image]
75   exact congrArg Subtype.val he
76 
77 def repair (x : E) (hx : Feasible D p x) : E := x - (leastCorrection D p x hx).val
78 
79 theorem repair_exact (x : E) (hx : Feasible D p x) : D (repair D p x hx) = 0 := by
80   rw [repair, map_sub]
81   exact sub_eq_zero.mpr (leastCorrection_image D p x hx).symm
82 
83 theorem repair_preserves (x : E) (hx : Feasible D p x) : p (repair D p x hx) = p x := by
84   have hz : p (leastCorrection D p x hx).val = 0 := (leastCorrection D p x hx).property
85   rw [repair, map_sub, hz, sub_zero]
86 
87 theorem displacement_norm (x : E) (hx : Feasible D p x) :
88     ‖x - repair D p x hx‖ = ‖leastCorrection D p x hx‖ := by
89   rw [repair, sub_sub_cancel]
90   rfl
91 
92 /-- The difference of any two permitted corrections is in the actual ambiguity kernel. -/
93 theorem correction_difference (x : E) (hx : Feasible D p x) (h : p.ker)
94     (hh : restricted D p h = D x) :
95     h - leastCorrection D p x hx ∈ (restricted D p).ker := by
96   change restricted D p (h - leastCorrection D p x hx) = 0
97   rw [map_sub, hh, leastCorrection_image, sub_self]
98 
99 theorem correction_pythagoras (x : E) (hx : Feasible D p x) (h : p.ker)
100     (hh : restricted D p h = D x) :
101     ‖h‖^2 = ‖leastCorrection D p x hx‖^2 + ‖h-leastCorrection D p x hx‖^2 := by
102   have ho : ⟪h-leastCorrection D p x hx, leastCorrection D p x hx⟫ = 0 :=
103     leastCorrection_orthogonal D p x hx _ (correction_difference D p x hx h hh)
104   have he := norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
105     (h-leastCorrection D p x hx) (leastCorrection D p x hx) ho
106   rw [sub_add_cancel] at he
107   simpa only [pow_two, add_comm] using he
108 
109 theorem repair_pythagoras (x : E) (hx : Feasible D p x) (y : E)
110     (hy : D y = 0) (hp : p y = p x) :
111     ‖x-y‖^2 = ‖x-repair D p x hx‖^2 + ‖repair D p x hx-y‖^2 := by
112   let h : p.ker := ⟨x-y, by change p (x-y)=0; rw [map_sub, hp, sub_self]⟩
113   have hh : restricted D p h = D x := by
114     change D (x-y) = D x
115     rw [map_sub, hy, sub_zero]
116   have he := correction_pythagoras D p x hx h hh
117   rw [displacement_norm]
118   have hn : ‖h-leastCorrection D p x hx‖ = ‖repair D p x hx-y‖ := by
119     change ‖(x-y)-(leastCorrection D p x hx).val‖ = ‖(x-(leastCorrection D p x hx).val)-y‖
120     congr 1
121     abel
122   rw [hn] at he
123   exact he
124 
125 theorem repair_best (x : E) (hx : Feasible D p x) (y : E)
126     (hy : D y = 0) (hp : p y = p x) :
127     ‖x-repair D p x hx‖ ≤ ‖x-y‖ := by
128   have he := repair_pythagoras D p x hx y hy hp
129   have h1 := norm_nonneg (x-repair D p x hx)
130   have h2 := norm_nonneg (x-y)
131   nlinarith [sq_nonneg ‖repair D p x hx-y‖]
132 
133 theorem repair_unique_nearest (x : E) (hx : Feasible D p x) (y : E)
134     (hy : D y = 0) (hp : p y = p x)
135     (hb : ‖x-y‖ ≤ ‖x-repair D p x hx‖) : y = repair D p x hx := by
136   have he := repair_pythagoras D p x hx y hy hp
137   have h1 := norm_nonneg (x-repair D p x hx)
138   have h2 := norm_nonneg (x-y)
139   have h3 := norm_nonneg (repair D p x hx-y)
140   have hz : ‖repair D p x hx-y‖ = 0 := by nlinarith
141   exact (sub_eq_zero.mp (norm_eq_zero.mp hz)).symm
142 
143 theorem exists_unique_nearest (x : E) (hx : Feasible D p x) :
144     ∃! y : E, D y = 0 ∧ p y = p x ∧
145       ∀ z : E, D z = 0 → p z = p x → ‖x-y‖ ≤ ‖x-z‖ := by
146   refine ⟨repair D p x hx,
147     ⟨repair_exact D p x hx, repair_preserves D p x hx, repair_best D p x hx⟩, ?_⟩
148   intro y hy
149   exact repair_unique_nearest D p x hx y hy.1 hy.2.1
150     (hy.2.2 _ (repair_exact D p x hx) (repair_preserves D p x hx))
151 
152 /-- On an admissible raw vector, protected displacement is the usual kernel displacement in M. -/
153 theorem leastCorrection_subtype (a : p.ker) (hx : Feasible D p a.val) :
154     leastCorrection D p a.val hx =
155       a - HilbertKernelProjection.projection (restricted D p) a := by
156   symm
157   apply leastCorrection_unique
158   · exact HilbertKernelProjection.defect_error _ a
159   · exact HilbertKernelProjection.error_orthogonal _ a
160 
161 variable [CompleteSpace R]
162 
163 /-- The transverse inverse norm for the restricted, rather than unconstrained, operator. -/
164 def gain (hc : IsClosed (Set.range (restricted D p))) : ℝ :=
165   HilbertKernelProjection.gain (restricted D p) hc
166 
167 theorem gain_nonneg (hc : IsClosed (Set.range (restricted D p))) : 0 ≤ gain D p hc :=
168   HilbertKernelProjection.gain_nonneg _ _
169 
170 theorem repair_bound (hc : IsClosed (Set.range (restricted D p)))
171     (x : E) (hx : Feasible D p x) :
172     ‖x-repair D p x hx‖ ≤ gain D p hc * ‖D x‖ := by
173   rw [displacement_norm]
174   have he := HilbertKernelProjection.complement_bound (restricted D p) hc
175     ⟨leastCorrection D p x hx, leastCorrection_orthogonal D p x hx⟩
176   simpa only [gain, leastCorrection_image] using he
177 
178 theorem closed_range_iff_protected_bound :
179     IsClosed (Set.range (restricted D p)) ↔
180       ∃ C : ℝ, 0 ≤ C ∧ ∀ (x : E) (hx : Feasible D p x),
181         ‖x-repair D p x hx‖ ≤ C * ‖D x‖ := by
182   constructor
183   · intro hc
184     exact ⟨gain D p hc, gain_nonneg D p hc, repair_bound D p hc⟩
185   · rintro ⟨C, hC, hb⟩
186     apply HilbertKernelProjection.closed_range_of_bound (restricted D p) C hC
187     intro a
188     have hx : Feasible D p a.val := ⟨a, rfl⟩
189     have he := hb a.val hx
190     rw [displacement_norm, leastCorrection_subtype] at he
191     exact he
192 
193 theorem gain_le_of_protected_bound (hc : IsClosed (Set.range (restricted D p)))
194     (C : ℝ) (hC : 0 ≤ C)
195     (hb : ∀ (x : E) (hx : Feasible D p x), ‖x-repair D p x hx‖ ≤ C*‖D x‖) :
196     gain D p hc ≤ C := by
197   apply HilbertKernelProjection.gain_le_of_bound (restricted D p) hc C hC
198   intro a
199   have hx : Feasible D p a.val := ⟨a, rfl⟩
200   have he := hb a.val hx
201   rw [displacement_norm, leastCorrection_subtype] at he
202   exact he
203 
204 theorem gain_characterization (hc : IsClosed (Set.range (restricted D p)))
205     (C : ℝ) (hC : 0 ≤ C) :
206     (∀ (x : E) (hx : Feasible D p x), ‖x-repair D p x hx‖ ≤ C*‖D x‖) ↔
207       gain D p hc ≤ C := by
208   constructor
209   · exact gain_le_of_protected_bound D p hc C hC
210   · intro h x hx
211     exact (repair_bound D p hc x hx).trans (mul_le_mul_of_nonneg_right h (norm_nonneg _))
212 
213 theorem gain_zero_iff (hc : IsClosed (Set.range (restricted D p))) :
214     gain D p hc = 0 ↔ restricted D p = 0 :=
215   HilbertKernelProjection.gain_eq_zero_iff _ _
216 
217 end KomorebiSpace.ProtectedHilbertRepair
218 end

Back to source controls