RegularizationNoiseLimits.lean

1 import KomorebiSpace.RegularizationStrongLimit
2 import Mathlib.Analysis.Normed.Group.Continuity
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Noisy data and inexact stopping limits
8 
9 The data and solver errors are measured for one fixed bounded linear operator
10 between the declared real Hilbert spaces. Parameter choices are limits along
11 arbitrary filters; in particular, they include a full positive real family.
12 -/
13 
14 noncomputable section
15 universe u v w
16 namespace KomorebiSpace.RegularizationNoiseLimits
17 open Filter
18 open scoped Topology RealInnerProductSpace
19 open RegularizedHilbertRepair
20 open RegularizationLimits
21 
22 /-- The one-dimensional operator attaining the universal correction-noise gain. -/
23 def scalarSharpOperator (α : ℝ) : ℝ →L[ℝ] ℝ :=
24   Real.sqrt α • ContinuousLinearMap.id ℝ ℝ
25 
26 theorem scalarSharpOperator_adjoint (α : ℝ) :
27     (scalarSharpOperator α).adjoint = scalarSharpOperator α := by
28   symm
29   apply (ContinuousLinearMap.eq_adjoint_iff _ _).2
30   intro x y
31   simp [scalarSharpOperator, mul_comm, mul_left_comm]
32 
33 /-- Sharpness holds at every positive parameter and for every scalar datum. -/
34 theorem scalar_correction_formula (α : ℝ) (hα : 0 < α) (r : ℝ) :
35     correction (scalarSharpOperator α) α hα r = r / (2 * Real.sqrt α) := by
36   symm
37   apply normal_unique
38   rw [normal_apply, scalarSharpOperator_adjoint]
39   simp only [scalarSharpOperator, smul_apply,
40     ContinuousLinearMap.id_apply, smul_eq_mul]
41   have hs : Real.sqrt α ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hα)
42   have hsq := Real.sq_sqrt hα.le
43   field_simp
44   rw [hsq]
45   ring
46 
47 theorem data_noise_coefficient_attained (α : ℝ) (hα : 0 < α) (r s : ℝ) :
48     ‖correction (scalarSharpOperator α) α hα r -
49       correction (scalarSharpOperator α) α hα s‖ = ‖r-s‖ / (2 * Real.sqrt α) := by
50   rw [scalar_correction_formula, scalar_correction_formula, ← sub_div, norm_div]
51   rw [Real.norm_of_nonneg (by positivity : 0 ≤ 2 * Real.sqrt α)]
52 
53 /-- Any universal scalar-data Lipschitz coefficient must be at least this value. -/
54 theorem data_noise_coefficient_le_of_uniform_bound (α K : ℝ) (hα : 0 < α)
55     (hK : ∀ r s : ℝ, ‖correction (scalarSharpOperator α) α hα r -
56       correction (scalarSharpOperator α) α hα s‖ ≤ K * ‖r-s‖) :
57     1 / (2 * Real.sqrt α) ≤ K := by
58   have h := hK 1 0
59   rw [data_noise_coefficient_attained] at h
60   simpa using h
61 
62 variable {H : Type u} {Y : Type v}
63 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
64 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
65 variable (T : H →L[ℝ] Y)
66 
67 /-- The stipulated data-error budget gives the sharp correction bound. -/
68 theorem noise_path_bound (r s : Y) {α δ : ℝ} (hα : 0 < α)
69     (hdata : ‖s-r‖ ≤ δ) :
70     ‖path T s α - path T r α‖ ≤ δ / (2 * Real.sqrt α) := by
71   rw [path_of_pos T s hα, path_of_pos T r hα]
72   exact (data_noise_bound T α hα s r).trans
73     (div_le_div_of_nonneg_right hdata (by positivity))
74 
75 /-- The fitted-data response has gain at most one. -/
76 theorem noise_fitted_path_bound (r s : Y) {α δ : ℝ} (hα : 0 < α)
77     (hdata : ‖s-r‖ ≤ δ) :
78     ‖T (path T s α - path T r α)‖ ≤ δ := by
79   rw [path_of_pos T s hα, path_of_pos T r hα]
80   exact (data_fitted_bound T α hα s r).trans hdata
81 
82 /-- The two budgets apply to the measured problem and to the same fixed operator. -/
83 theorem solver_data_path_bound (r s : Y) (a : H) {α δ ε : ℝ} (hα : 0 < α)
84     (hdata : ‖s-r‖ ≤ δ) (hsolver : ‖gradient T α s a‖ ≤ ε) :
85     ‖a-path T r α‖ ≤ ε/α + δ/(2*Real.sqrt α) := by
86   rw [path_of_pos T r hα]
87   exact (solver_and_data_bound T α hα r s a).trans
88     (add_le_add (div_le_div_of_nonneg_right hsolver hα.le)
89       (div_le_div_of_nonneg_right hdata (by positivity)))
90 
91 /-- The pointwise stopping certificate separates solver error, noise, and bias. -/
92 theorem stopping_three_term_bound (r s : Y) (a aMin : H) {α δ ε : ℝ} (hα : 0 < α)
93     (hdata : ‖s-r‖ ≤ δ) (hsolver : ‖gradient T α s a‖ ≤ ε) :
94     ‖a-aMin‖ ≤ ε/α + δ/(2*Real.sqrt α) + ‖path T r α-aMin‖ := by
95   have he : a-aMin = (a-path T r α)+(path T r α-aMin) := by abel
96   calc
97     ‖a-aMin‖ = ‖(a-path T r α)+(path T r α-aMin)‖ := by rw [he]
98     _ ≤ ‖a-path T r α‖+‖path T r α-aMin‖ := norm_add_le _ _
99     _ ≤ _ := add_le_add (solver_data_path_bound T r s a hα hdata hsolver) le_rfl
100 
101 variable {I : Type w} {l : Filter I}
102 
103 theorem noise_half_ratio_tendsto {α δ : I → ℝ}
104     (hnoise : Tendsto (fun i => δ i / Real.sqrt (α i)) l (𝓝 0)) :
105     Tendsto (fun i => δ i / (2 * Real.sqrt (α i))) l (𝓝 0) := by
106   have he : (fun i => δ i / (2 * Real.sqrt (α i))) =
107       (fun i => (δ i / Real.sqrt (α i)) / 2) := by
108     funext i
109     ring
110   rw [he]
111   simpa only [zero_div] using hnoise.div_const 2
112 
113 /-- Vanishing propagated data error transfers an exact-data strong limit. -/
114 theorem noisy_tendsto_of_exact_tendsto (r : Y) (s : I → Y) (aMin : H)
115     (α δ : I → ℝ) (hα : ∀ᶠ i in l, 0 < α i)
116     (hdata : ∀ᶠ i in l, ‖s i-r‖ ≤ δ i)
117     (hnoise : Tendsto (fun i => δ i / Real.sqrt (α i)) l (𝓝 0))
118     (hbias : Tendsto (fun i => path T r (α i)) l (𝓝 aMin)) :
119     Tendsto (fun i => path T (s i) (α i)) l (𝓝 aMin) := by
120   have hbound : ∀ᶠ i in l, ‖path T (s i) (α i)-path T r (α i)‖ ≤
121       δ i / (2*Real.sqrt (α i)) := by
122     filter_upwards [hα, hdata] with i hi hd
123     exact noise_path_bound T r (s i) hi hd
124   have hdiff := squeeze_zero_norm' hbound (noise_half_ratio_tendsto hnoise)
125   simpa only [sub_add_cancel, zero_add] using hdiff.add hbias
126 
127 /-- Solver residuals and data errors may vary independently along any filter. -/
128 theorem inexact_tendsto_of_exact_tendsto (r : Y) (s : I → Y) (a : I → H) (aMin : H)
129     (α δ ε : I → ℝ) (hα : ∀ᶠ i in l, 0 < α i)
130     (hdata : ∀ᶠ i in l, ‖s i-r‖ ≤ δ i)
131     (hsolver : ∀ᶠ i in l, ‖gradient T (α i) (s i) (a i)‖ ≤ ε i)
132     (hnoise : Tendsto (fun i => δ i / Real.sqrt (α i)) l (𝓝 0))
133     (hsolve : Tendsto (fun i => ε i / α i) l (𝓝 0))
134     (hbias : Tendsto (fun i => path T r (α i)) l (𝓝 aMin)) :
135     Tendsto a l (𝓝 aMin) := by
136   have hbound : ∀ᶠ i in l, ‖a i-path T r (α i)‖ ≤
137       ε i/α i + δ i/(2*Real.sqrt (α i)) := by
138     filter_upwards [hα, hdata, hsolver] with i hi hd hs
139     exact solver_data_path_bound T r (s i) (a i) hi hd hs
140   have hsum : Tendsto (fun i => ε i/α i + δ i/(2*Real.sqrt (α i))) l (𝓝 0) := by
141     simpa only [zero_add] using hsolve.add (noise_half_ratio_tendsto hnoise)
142   have hdiff := squeeze_zero_norm' hbound hsum
143   simpa only [sub_add_cancel, zero_add] using hdiff.add hbias
144 
145 /-- The attained-projection theorem supplies the bias limit for any parameter choice. -/
146 theorem noisy_parameter_choice (r : Y) (s : I → Y) (aMin : H) (α δ : I → ℝ)
147     (ha : T aMin = BudgetProfile.projectedDatum T r)
148     (hmin : ∀ x : H, T x = BudgetProfile.projectedDatum T r → ‖aMin‖ ≤ ‖x‖)
149     (hα : Tendsto α l (𝓝[>] (0 : ℝ)))
150     (hdata : ∀ᶠ i in l, ‖s i-r‖ ≤ δ i)
151     (hnoise : Tendsto (fun i => δ i / Real.sqrt (α i)) l (𝓝 0)) :
152     Tendsto (fun i => path T (s i) (α i)) l (𝓝 aMin) := by
153   apply noisy_tendsto_of_exact_tendsto T r s aMin α δ
154     (hα.eventually self_mem_nhdsWithin) hdata hnoise
155   exact (RegularizationStrongLimit.path_tendsto_of_minimum T r aMin ha hmin).comp hα
156 
157 /-- WR09 for the entire positive noise-level family, not just a selected sequence. -/
158 theorem noisy_parameter_choice_nhdsWithin (r : Y) (s : ℝ → Y) (aMin : H) (α : ℝ → ℝ)
159     (ha : T aMin = BudgetProfile.projectedDatum T r)
160     (hmin : ∀ x : H, T x = BudgetProfile.projectedDatum T r → ‖aMin‖ ≤ ‖x‖)
161     (hpos : ∀ δ : ℝ, 0 < δ → 0 < α δ)
162     (hα : Tendsto α (𝓝[>] (0 : ℝ)) (𝓝 0))
163     (hdata : ∀ δ : ℝ, 0 < δ → ‖s δ-r‖ ≤ δ)
164     (hnoise : Tendsto (fun δ => δ / Real.sqrt (α δ)) (𝓝[>] (0 : ℝ)) (𝓝 0)) :
165     Tendsto (fun δ => path T (s δ) (α δ)) (𝓝[>] (0 : ℝ)) (𝓝 aMin) := by
166   have hpos' : ∀ᶠ δ in 𝓝[>] (0 : ℝ), 0 < α δ := by
167     filter_upwards [self_mem_nhdsWithin] with δ hδ
168     exact hpos δ hδ
169   have hdata' : ∀ᶠ δ in 𝓝[>] (0 : ℝ), ‖s δ-r‖ ≤ δ := by
170     filter_upwards [self_mem_nhdsWithin] with δ hδ
171     exact hdata δ hδ
172   exact noisy_parameter_choice T r s aMin α id ha hmin
173     (tendsto_nhdsWithin_iff.mpr ⟨hα, hpos'⟩) hdata' hnoise
174 
175 /-- WR16 for arbitrary filtered schedules of measured and inexact problems. -/
176 theorem inexact_parameter_choice (r : Y) (s : I → Y) (a : I → H) (aMin : H)
177     (α δ ε : I → ℝ)
178     (ha : T aMin = BudgetProfile.projectedDatum T r)
179     (hmin : ∀ x : H, T x = BudgetProfile.projectedDatum T r → ‖aMin‖ ≤ ‖x‖)
180     (hα : Tendsto α l (𝓝[>] (0 : ℝ)))
181     (hdata : ∀ᶠ i in l, ‖s i-r‖ ≤ δ i)
182     (hsolver : ∀ᶠ i in l, ‖gradient T (α i) (s i) (a i)‖ ≤ ε i)
183     (hnoise : Tendsto (fun i => δ i / Real.sqrt (α i)) l (𝓝 0))
184     (hsolve : Tendsto (fun i => ε i / α i) l (𝓝 0)) :
185     Tendsto a l (𝓝 aMin) := by
186   apply inexact_tendsto_of_exact_tendsto T r s a aMin α δ ε
187     (hα.eventually self_mem_nhdsWithin) hdata hsolver hnoise hsolve
188   exact (RegularizationStrongLimit.path_tendsto_of_minimum T r aMin ha hmin).comp hα
189 
190 /-- The printed sequence stopping rule, with its full three-term certificate at every index. -/
191 theorem stopping_rule_sequence (r : Y) (s : ℕ → Y) (a : ℕ → H) (aMin : H)
192     (α δ ε : ℕ → ℝ)
193     (ha : T aMin = BudgetProfile.projectedDatum T r)
194     (hmin : ∀ x : H, T x = BudgetProfile.projectedDatum T r → ‖aMin‖ ≤ ‖x‖)
195     (hpos : ∀ n, 0 < α n) (hα : Tendsto α atTop (𝓝 0))
196     (hdata : ∀ n, ‖s n-r‖ ≤ δ n)
197     (hsolver : ∀ n, ‖gradient T (α n) (s n) (a n)‖ ≤ ε n)
198     (hnoise : Tendsto (fun n => δ n / Real.sqrt (α n)) atTop (𝓝 0))
199     (hsolve : Tendsto (fun n => ε n / α n) atTop (𝓝 0)) :
200     Tendsto a atTop (𝓝 aMin) ∧ ∀ n,
201       ‖a n-aMin‖ ≤ ε n/α n + δ n/(2*Real.sqrt (α n)) + ‖path T r (α n)-aMin‖ := by
202   refine ⟨?_, fun n => stopping_three_term_bound T r (s n) (a n) aMin
203     (hpos n) (hdata n) (hsolver n)⟩
204   exact inexact_parameter_choice T r s a aMin α δ ε ha hmin
205     (tendsto_nhdsWithin_iff.mpr ⟨hα, Eventually.of_forall hpos⟩)
206     (Eventually.of_forall hdata) (Eventually.of_forall hsolver) hnoise hsolve
207 
208 end KomorebiSpace.RegularizationNoiseLimits

Back to source controls