ResidualPerturbation.lean

1 import KomorebiSpace.HilbertKernelProjection
2 import Mathlib.Tactic.Linarith
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Robust residual certificates
8 
9 Measurement error, operator error, and change of the exact kernel are separated.
10 A common-kernel conclusion is derived from preservation of the old kernel and a
11 strict perturbation budget. Without preservation, the bound is to the old exact
12 space and includes an input-size term. No noisy value is reclassified as exact.
13 -/
14 universe u v
15 noncomputable section
16 namespace KomorebiSpace
17 namespace ResidualRobustness
18 open HilbertKernelProjection
19 variable {E : Type u} {R : Type v}
20 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
21 variable [NormedAddCommGroup R] [NormedSpace ℝ R]
22 
23 /-- Evidence about the actual canonical projection, not a numerical success flag. -/
24 structure Bound (d : E →L[ℝ] R) where
25   constant : ℝ
26   nonneg : 0 ≤ constant
27   estimate : ∀ x, ‖x-projection d x‖ ≤ constant*‖d x‖
28 
29 namespace Bound
30 variable {d : E →L[ℝ] R} (B : Bound d)
31 
32 /-- A certified residual ball bounds the distance to the original exact space. -/
33 theorem measured (x : E) (y : R) (η : ℝ) (hy : ‖d x-y‖≤η) :
34     ‖x-projection d x‖≤B.constant*(‖y‖+η) := by
35   apply (B.estimate x).trans
36   apply mul_le_mul_of_nonneg_left _ B.nonneg
37   calc
38     ‖d x‖ ≤ ‖d x-y‖+‖y‖ := by
39       simpa only [sub_add_cancel] using norm_add_le (d x-y) y
40     _ ≤ ‖y‖+η := by linarith
41 
42 /-- With no kernel-preservation assumption, operator error costs epsilon times
43 input size. The conclusion still concerns the reference exact space. -/
44 theorem uncertain_operator (e : E →L[ℝ] R) (ε η : ℝ)
45     (he : ∀ x, ‖(d-e) x‖≤ε*‖x‖) (x : E) (y : R) (hy : ‖e x-y‖≤η) :
46     ‖x-projection d x‖≤B.constant*(‖y‖+η+ε*‖x‖) := by
47   apply (B.estimate x).trans
48   apply mul_le_mul_of_nonneg_left _ B.nonneg
49   have ht : ‖d x‖≤‖(d-e) x‖+‖e x-y‖+‖y‖ := by
50     have h := norm_add_le ((d-e) x) (e x-y)
51     have h' := norm_add_le ((d-e) x+(e x-y)) y
52     have hid : (d-e) x+(e x-y)+y=d x := by simp only [sub_apply]; abel
53     rw [hid] at h'
54     linarith
55   have hp := he x
56   linarith
57 
58 /-- Operator-norm uncertainty implies the pointwise estimate used above. -/
59 theorem uncertain_operator_opNorm (e : E →L[ℝ] R) (ε η : ℝ)
60     (he : ‖d-e‖≤ε) (x : E) (y : R) (hy : ‖e x-y‖≤η) :
61     ‖x-projection d x‖≤B.constant*(‖y‖+η+ε*‖x‖) :=
62   B.uncertain_operator e ε η (fun z => ((d-e).le_opNorm z).trans
63     (mul_le_mul_of_nonneg_right he (norm_nonneg z))) x y hy
64 
65 /-- The direction of exact-space comparison that needs no preservation premise. -/
66 theorem new_exact_near_old (e : E →L[ℝ] R) (ε : ℝ)
67     (he : ∀ x, ‖(d-e) x‖≤ε*‖x‖) (x : E) (hx : e x=0) :
68     ‖x-projection d x‖≤B.constant*ε*‖x‖ := by
69   have h := B.uncertain_operator e ε 0 he x 0 (by simp [hx])
70   simpa only [norm_zero,add_zero,zero_add,mul_assoc] using h
71 
72 /-- A preserved exact component plus a strict radius excludes new null modes. -/
73 theorem preserved_kernel_bound (e : E →L[ℝ] R) (ε : ℝ)
74     (he : ∀ x, ‖(d-e) x‖≤ε*‖x‖)
75     (hpres : ∀ x, e (projection d x)=0) (hradius : B.constant*ε<1) (x : E) :
76     ‖x-projection d x‖≤(B.constant/(1-B.constant*ε))*‖e x‖ := by
77   let u := x-projection d x
78   have hdu : d u=d x := defect_error d x
79   have heu : e u=e x := by simp only [u,map_sub,hpres,sub_zero]
80   have htri : ‖d x‖≤‖e x‖+ε*‖u‖ := by
81     calc
82       ‖d x‖ = ‖(d-e) u+e u‖ := by simp only [sub_apply,sub_add_cancel,hdu]
83       _ ≤ ‖(d-e) u‖+‖e u‖ := norm_add_le _ _
84       _ ≤ ‖e x‖+ε*‖u‖ := by rw [heu]; linarith [he u]
85   have hb := (B.estimate x).trans (mul_le_mul_of_nonneg_left htri B.nonneg)
86   have hp : 0<1-B.constant*ε := sub_pos.mpr hradius
87   have hh : (1-B.constant*ε)*‖x-projection d x‖≤B.constant*‖e x‖ := by
88     dsimp only [u] at hb
89     nlinarith
90   calc
91     _ ≤ (B.constant*‖e x‖)/(1-B.constant*ε) :=
92       (le_div_iff₀ hp).mpr (by nlinarith [hh])
93     _ = _ := by ring
94 
95 /-- Equality of kernels is a conclusion, not an input field. -/
96 theorem kernels_equal (e : E →L[ℝ] R) (ε : ℝ)
97     (he : ∀ x, ‖(d-e) x‖≤ε*‖x‖)
98     (hpres : ∀ x, e (projection d x)=0) (hradius : B.constant*ε<1) : d.ker=e.ker := by
99   ext x
100   change d x=0 ↔ e x=0
101   constructor
102   · intro hx
103     simpa only [projection_fixes d x hx] using hpres x
104   · intro hx
105     have hb := B.preserved_kernel_bound e ε he hpres hradius x
106     rw [hx,norm_zero,mul_zero] at hb
107     have hz : x=projection d x := sub_eq_zero.mp (norm_eq_zero.mp
108       (le_antisymm hb (norm_nonneg _)))
109     rw [hz]
110     exact projection_exact d x
111 
112 /-- The same canonical exact repair works for every admitted perturbation. -/
113 theorem projections_equal (e : E →L[ℝ] R) (ε : ℝ)
114     (he : ∀ x, ‖(d-e) x‖≤ε*‖x‖)
115     (hpres : ∀ x, e (projection d x)=0) (hradius : B.constant*ε<1) :
116     projection d=projection e :=
117   projection_eq_of_kernel_eq d e (B.kernels_equal e ε he hpres hradius)
118 
119 /-- A robustness certificate with an explicitly degraded gain. -/
120 def perturb (e : E →L[ℝ] R) (ε : ℝ)
121     (he : ∀ x, ‖(d-e) x‖≤ε*‖x‖)
122     (hpres : ∀ x, e (projection d x)=0) (hradius : B.constant*ε<1) : Bound e where
123   constant := B.constant/(1-B.constant*ε)
124   nonneg := div_nonneg B.nonneg (le_of_lt (sub_pos.mpr hradius))
125   estimate x := by
126     rw [← B.projections_equal e ε he hpres hradius]
127     exact B.preserved_kernel_bound e ε he hpres hradius x
128 
129 /-- The perturbed range is closed under the same explicit assumptions. -/
130 theorem perturbed_closed_range (e : E →L[ℝ] R) (ε : ℝ)
131     (he : ∀ x, ‖(d-e) x‖≤ε*‖x‖)
132     (hpres : ∀ x, e (projection d x)=0) (hradius : B.constant*ε<1) :
133     IsClosed (Set.range e) :=
134   closed_range_of_bound e (B.perturb e ε he hpres hradius).constant
135     (B.perturb e ε he hpres hradius).nonneg
136     (B.perturb e ε he hpres hradius).estimate
137 
138 /-- Measurement uncertainty for a kernel-preserving operator perturbation. -/
139 theorem perturbed_measured (e : E →L[ℝ] R) (ε η : ℝ)
140     (he : ∀ x, ‖(d-e) x‖≤ε*‖x‖)
141     (hpres : ∀ x, e (projection d x)=0) (hradius : B.constant*ε<1)
142     (x : E) (y : R) (hy : ‖e x-y‖≤η) :
143     ‖x-projection d x‖≤(B.constant/(1-B.constant*ε))*(‖y‖+η) := by
144   have h := (B.perturb e ε he hpres hradius).measured x y η hy
145   simpa only [perturb,← B.projections_equal e ε he hpres hradius] using h
146 
147 end Bound
148 end ResidualRobustness
149 end KomorebiSpace
150 end

Back to source controls