RegularizationLimits.lean

1 import KomorebiSpace.RegularizedHilbertRepair
2 import KomorebiSpace.BudgetProfile
3 
4 /-!
5 # The small-parameter regularization limits (WR08)
6 
7 The limit is over all positive real parameters approaching zero. The projected
8 datum belongs to the closure of the operator range; no closed-range assumption
9 is made. Unattained projected data force divergence of the correction norms.
10 -/
11 
12 noncomputable section
13 
14 open Filter Set Metric
15 open scoped Topology
16 
17 namespace KomorebiSpace.RegularizationLimits
18 
19 open BudgetProfile
20 
21 variable {H Y : Type*}
22 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
23 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
24 
25 /-- A total parameter path, using the established regularized correction at every
26 positive parameter. Its values elsewhere do not affect the right-hand limit. -/
27 def path (T : H →L[ℝ] Y) (r : Y) (α : ℝ) : H :=
28   if h : 0 < α then RegularizedHilbertRepair.correction T α h r else 0
29 
30 theorem path_of_pos (T : H →L[ℝ] Y) (r : Y) {α : ℝ} (hα : 0 < α) :
31     path T r α = RegularizedHilbertRepair.correction T α hα r := by
32   simp only [path, dite_eq_left hα]
33 
34 theorem eventual_pos : ∀ᶠ α : ℝ in 𝓝[>] 0, 0 < α :=
35   self_mem_nhdsWithin
36 
37 /-- Canceling the orthogonal residual floor in the global objective comparison. -/
38 theorem objective_comparison (T : H →L[ℝ] Y) (r : Y) {α : ℝ}
39     (hα : 0 < α) (a : H) :
40     ‖projectedDatum T r - T (path T r α)‖ ^ 2 + α * ‖path T r α‖ ^ 2 ≤
41       ‖projectedDatum T r - T a‖ ^ 2 + α * ‖a‖ ^ 2 := by
42   rw [path_of_pos T r hα]
43   have hb := RegularizedHilbertRepair.correction_best T α hα r a
44   unfold RegularizedHilbertRepair.objective at hb
45   rw [norm_sub_rev (T (RegularizedHilbertRepair.correction T α hα r)) r,
46     norm_sub_rev (T a) r, residual_sq_decomposition T r,
47     residual_sq_decomposition T r] at hb
48   linarith
49 
50 /-- The projected fitting error and weighted correction penalty vanish together. -/
51 theorem projected_energy_tendsto_zero (T : H →L[ℝ] Y) (r : Y) :
52     Tendsto (fun α : ℝ =>
53       ‖projectedDatum T r - T (path T r α)‖ ^ 2 + α * ‖path T r α‖ ^ 2)
54       (𝓝[>] 0) (𝓝 0) := by
55   apply Metric.tendsto_nhds.mpr
56   intro ε hε
57   have hhalf : 0 < ε / 2 := by linarith
58   have hclosure : projectedDatum T r ∈ closure (Set.range T) :=
59     projectedDatum_mem T r
60   obtain ⟨_, ⟨a, rfl⟩, ha⟩ :=
61     Metric.mem_closure_iff.mp hclosure (Real.sqrt (ε / 2)) (Real.sqrt_pos.mpr hhalf)
62   rw [dist_eq_norm] at ha
63   have hsq : ‖projectedDatum T r - T a‖ ^ 2 < ε / 2 := by
64     nlinarith [Real.sq_sqrt hhalf.le, norm_nonneg (projectedDatum T r - T a),
65       Real.sqrt_nonneg (ε / 2)]
66   have hm : Tendsto (fun α : ℝ => α * ‖a‖ ^ 2) (𝓝[>] 0) (𝓝 0) := by
67     simpa only [zero_mul, id_eq] using
68       (tendsto_nhdsWithin_of_tendsto_nhds
69         (tendsto_id : Tendsto (fun α : ℝ => α) (𝓝 0) (𝓝 0))).mul_const (‖a‖ ^ 2)
70   filter_upwards [eventual_pos, (tendsto_order.mp hm).2 (ε / 2) hhalf] with α hα hsmall
71   have hlo : 0 ≤ ‖projectedDatum T r - T (path T r α)‖ ^ 2 +
72       α * ‖path T r α‖ ^ 2 :=
73     add_nonneg (sq_nonneg _) (mul_nonneg hα.le (sq_nonneg _))
74   rw [Real.dist_eq, sub_zero, abs_of_nonneg hlo]
75   have hcomp := objective_comparison T r hα a
76   linarith
77 
78 theorem projected_error_sq_tendsto_zero (T : H →L[ℝ] Y) (r : Y) :
79     Tendsto (fun α : ℝ => ‖projectedDatum T r - T (path T r α)‖ ^ 2)
80       (𝓝[>] 0) (𝓝 0) := by
81   apply squeeze_zero' (Filter.Eventually.of_forall fun _ => sq_nonneg _)
82     ?_ (projected_energy_tendsto_zero T r)
83   filter_upwards [eventual_pos] with α hα
84   exact le_add_of_nonneg_right (mul_nonneg hα.le (sq_nonneg _))
85 
86 /-- The full positive-parameter family converges to the range-closure projection. -/
87 theorem fitted_tendsto_projectedDatum (T : H →L[ℝ] Y) (r : Y) :
88     Tendsto (fun α : ℝ => T (path T r α)) (𝓝[>] 0) (𝓝 (projectedDatum T r)) := by
89   apply tendsto_iff_norm_sub_tendsto_zero.mpr
90   have h := (projected_error_sq_tendsto_zero T r).sqrt
91   simpa only [Real.sqrt_sq (norm_nonneg _), Real.sqrt_zero, norm_sub_rev] using h
92 
93 /-- The residual norm tends to the unavoidable orthogonal residual floor. -/
94 theorem residual_norm_tendsto_floor (T : H →L[ℝ] Y) (r : Y) :
95     Tendsto (fun α : ℝ => ‖r - T (path T r α)‖) (𝓝[>] 0)
96       (𝓝 ‖r - projectedDatum T r‖) :=
97   (tendsto_const_nhds.sub (fitted_tendsto_projectedDatum T r)).norm
98 
99 /-- Vanishing weighted penalty does not assert bounded correction norms. -/
100 theorem weighted_penalty_tendsto_zero (T : H →L[ℝ] Y) (r : Y) :
101     Tendsto (fun α : ℝ => α * ‖path T r α‖ ^ 2) (𝓝[>] 0) (𝓝 0) := by
102   apply squeeze_zero' ?_ (Filter.Eventually.of_forall fun _ => le_add_of_nonneg_left
103     (sq_nonneg _)) (projected_energy_tendsto_zero T r)
104   filter_upwards [eventual_pos] with α hα
105   exact mul_nonneg hα.le (sq_nonneg _)
106 
107 /-- If the projected datum is unattained, the norms escape every finite budget
108 along the whole right-hand parameter filter, not merely along a sequence. -/
109 theorem norm_tendsto_atTop_of_not_mem_range (T : H →L[ℝ] Y) (r : Y)
110     (hr : projectedDatum T r ∉ Set.range T) :
111     Tendsto (fun α : ℝ => ‖path T r α‖) (𝓝[>] 0) atTop := by
112   apply Filter.tendsto_atTop.mpr
113   intro M
114   by_contra h
115   have hfreq : ∃ᶠ α : ℝ in 𝓝[>] 0, ‖path T r α‖ ≤ M :=
116     (Filter.not_eventually.mp h).mono fun _ hn => (lt_of_not_ge hn).le
117   obtain ⟨a, ha, _⟩ := BoundedApproximateRealization.exists_solution_of_frequently_bounded
118     T (path T r) (projectedDatum T r) M hfreq (fitted_tendsto_projectedDatum T r)
119   exact hr ⟨a, ha⟩
120 
121 end KomorebiSpace.RegularizationLimits

Back to source controls