RegularizationStrongLimit.lean

1 import KomorebiSpace.RegularizationLimits
2 import KomorebiSpace.NestedMinimumCorrections
3 
4 /-!
5 # Strong regularization limit at an attainable projected datum (WR08)
6 
7 The minimum norm preimage is constructed from the closed convex fiber. A
8 frequently bounded version of WR01 supplies the lower norm limit; the exact
9 regularized energy identity then upgrades norm convergence to strong convergence.
10 -/
11 
12 noncomputable section
13 
14 open Filter Set Topology
15 
16 namespace KomorebiSpace.RegularizationStrongLimit
17 
18 variable {H Y : Type*}
19 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
20 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
21 
22 omit [CompleteSpace Y] in
23 /-- A nonempty operator fiber has a unique minimum norm element, even when the
24 operator range is not closed. -/
25 theorem exists_unique_minimum_preimage (T : H →L[ℝ] Y) (b : Y)
26     (hb : b ∈ Set.range T) :
27     ∃! a : H, T a = b ∧ ∀ x : H, T x = b → ‖a‖ ≤ ‖x‖ := by
28   have hne : (T ⁻¹' {b}).Nonempty := by
29     obtain ⟨x, hx⟩ := hb
30     exact ⟨x, hx⟩
31   have hc : IsClosed (T ⁻¹' {b}) := isClosed_singleton.preimage T.continuous
32   have hcv : Convex ℝ (T ⁻¹' {b}) := (convex_singleton b).linear_preimage T.toLinearMap
33   obtain ⟨a, ha⟩ := NestedMinimumCorrections.exists_minimum (T ⁻¹' {b}) hne hc hcv
34   refine ⟨a, ha, ?_⟩
35   intro x hx
36   exact NestedMinimumCorrections.minimum_unique hcv hx ha
37 
38 /-- The least norm compatible datum forces a lower norm limit for every
39 approximating filter, without selecting a weakly convergent subsequence. -/
40 theorem norm_tendsto_of_minimum (T : H →L[ℝ] Y) (b : Y) (a : H)
41     (hmin : ∀ x : H, T x = b → ‖a‖ ≤ ‖x‖)
42     {ι : Type*} {l : Filter ι} [NeBot l] (u : ι → H)
43     (himage : Tendsto (fun i => T (u i)) l (𝓝 b))
44     (hbound : ∀ᶠ i in l, ‖u i‖ ≤ ‖a‖) :
45     Tendsto (fun i => ‖u i‖) l (𝓝 ‖a‖) := by
46   apply tendsto_order.mpr
47   constructor
48   · intro c hc
49     by_contra h
50     have hfreq : ∃ᶠ i in l, ‖u i‖ ≤ c := by
51       simpa only [not_lt] using Filter.not_eventually.mp h
52     obtain ⟨x, hx, hxc⟩ :=
53       BoundedApproximateRealization.exists_solution_of_frequently_bounded T u b c hfreq himage
54     exact (not_le_of_gt hc) ((hmin x hx).trans hxc)
55   · intro c hc
56     exact hbound.mono fun i hi => hi.trans_lt hc
57 
58 omit [InnerProductSpace ℝ H] [CompleteSpace H] in
59 /-- An energy bound turns convergence of norms into convergence of vectors. -/
60 theorem tendsto_of_norm_energy_le {ι : Type*} {l : Filter ι} (u : ι → H) (a : H)
61     (hnorm : Tendsto (fun i => ‖u i‖) l (𝓝 ‖a‖))
62     (henergy : ∀ᶠ i in l, ‖u i - a‖ ^ 2 ≤ ‖a‖ ^ 2 - ‖u i‖ ^ 2) :
63     Tendsto u l (𝓝 a) := by
64   have he : Tendsto (fun i => ‖a‖ ^ 2 - ‖u i‖ ^ 2) l (𝓝 0) := by
65     simpa using (tendsto_const_nhds :
66       Tendsto (fun _ : ι => ‖a‖ ^ 2) l (𝓝 (‖a‖ ^ 2))).sub (hnorm.pow 2)
67   apply Metric.tendsto_nhds.mpr
68   intro ε hε
69   have hb : ∀ᶠ i in l, ‖a‖ ^ 2 - ‖u i‖ ^ 2 < ε ^ 2 :=
70     he.eventually (gt_mem_nhds (sq_pos_of_pos hε))
71   filter_upwards [henergy, hb] with i hi hib
72   rw [dist_eq_norm]
73   nlinarith [norm_nonneg (u i - a)]
74 
75 /-- Exact energy comparison bounds correction distance by the difference of
76 norm energies at any preimage of the projected datum. -/
77 theorem correction_distance_sq_le (T : H →L[ℝ] Y) (r : Y) {α : ℝ}
78     (hα : 0 < α) (a : H) (ha : T a = BudgetProfile.projectedDatum T r) :
79     ‖RegularizedHilbertRepair.correction T α hα r - a‖ ^ 2 ≤
80       ‖a‖ ^ 2 - ‖RegularizedHilbertRepair.correction T α hα r‖ ^ 2 := by
81   have he := RegularizedHilbertRepair.energy_identity T α hα r a
82   have hr := BudgetProfile.residual_sq_decomposition T r
83     (RegularizedHilbertRepair.correction T α hα r)
84   unfold RegularizedHilbertRepair.objective at he
85   rw [ha, norm_sub_rev (BudgetProfile.projectedDatum T r) r,
86     norm_sub_rev (T (RegularizedHilbertRepair.correction T α hα r)) r,
87     norm_sub_rev a (RegularizedHilbertRepair.correction T α hα r)] at he
88   nlinarith [sq_nonneg ‖T (a - RegularizedHilbertRepair.correction T α hα r)‖,
89     sq_nonneg ‖BudgetProfile.projectedDatum T r -
90       T (RegularizedHilbertRepair.correction T α hα r)‖]
91 
92 /-- The regularized correction stays within every exact projected-data budget. -/
93 theorem correction_norm_le (T : H →L[ℝ] Y) (r : Y) {α : ℝ}
94     (hα : 0 < α) (a : H) (ha : T a = BudgetProfile.projectedDatum T r) :
95     ‖RegularizedHilbertRepair.correction T α hα r‖ ≤ ‖a‖ := by
96   have he := correction_distance_sq_le T r hα a ha
97   nlinarith [sq_nonneg ‖RegularizedHilbertRepair.correction T α hα r - a‖,
98     norm_nonneg (RegularizedHilbertRepair.correction T α hα r), norm_nonneg a]
99 
100 /-- When the projected datum is attained, the entire positive-parameter path
101 converges in norm to its minimum norm preimage. -/
102 theorem path_tendsto_of_minimum (T : H →L[ℝ] Y) (r : Y) (a : H)
103     (ha : T a = BudgetProfile.projectedDatum T r)
104     (hmin : ∀ x : H, T x = BudgetProfile.projectedDatum T r → ‖a‖ ≤ ‖x‖) :
105     Tendsto (RegularizationLimits.path T r) (𝓝[>] (0 : ℝ)) (𝓝 a) := by
106   have hbound : ∀ᶠ α : ℝ in 𝓝[>] 0, ‖RegularizationLimits.path T r α‖ ≤ ‖a‖ := by
107     filter_upwards [RegularizationLimits.eventual_pos] with α hα
108     rw [RegularizationLimits.path_of_pos T r hα]
109     exact correction_norm_le T r hα a ha
110   have hnorm := norm_tendsto_of_minimum T (BudgetProfile.projectedDatum T r) a hmin
111     (RegularizationLimits.path T r)
112     (RegularizationLimits.fitted_tendsto_projectedDatum T r) hbound
113   apply tendsto_of_norm_energy_le (RegularizationLimits.path T r) a hnorm
114   filter_upwards [RegularizationLimits.eventual_pos] with α hα
115   rw [RegularizationLimits.path_of_pos T r hα]
116   exact correction_distance_sq_le T r hα a ha
117 
118 /-- WR08 attained case, constructing the unique minimum norm limit from range
119 membership rather than assuming its existence. -/
120 theorem exists_unique_minimum_and_limit (T : H →L[ℝ] Y) (r : Y)
121     (hb : BudgetProfile.projectedDatum T r ∈ Set.range T) :
122     ∃! a : H,
123       (T a = BudgetProfile.projectedDatum T r ∧
124         ∀ x : H, T x = BudgetProfile.projectedDatum T r → ‖a‖ ≤ ‖x‖) ∧
125       Tendsto (RegularizationLimits.path T r) (𝓝[>] (0 : ℝ)) (𝓝 a) := by
126   obtain ⟨a, ha, huniq⟩ :=
127     exists_unique_minimum_preimage T (BudgetProfile.projectedDatum T r) hb
128   refine ⟨a, ⟨ha, path_tendsto_of_minimum T r a ha.1 ha.2⟩, ?_⟩
129   intro x hx
130   exact huniq x hx.1
131 
132 end KomorebiSpace.RegularizationStrongLimit

Back to source controls