BudgetProfile.lean

1 import KomorebiSpace.BoundedApproximateRealization
2 import Mathlib.Analysis.InnerProductSpace.Projection.Basic
3 import Mathlib.Analysis.InnerProductSpace.Projection.Minimal
4 import Mathlib.Analysis.Convex.Function
5 import Mathlib.Topology.MetricSpace.HausdorffDistance
6 import Mathlib.Topology.Sequences
7 import Mathlib.Tactic
8 
9 /-!
10 # The attained residual at a fixed correction budget (WR03)
11 
12 The fixed-budget image is closed without a closed-range assumption, by the
13 accepted same-budget realization theorem. Hilbert projection then gives the
14 minimum at every nonnegative budget, including zero.
15 -/
16 
17 noncomputable section
18 
19 open Filter Set Metric
20 open scoped Topology
21 
22 namespace KomorebiSpace.BudgetProfile
23 
24 variable {H Y : Type*}
25 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
26 variable [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace Y]
27 
28 /-- The residual distance to the image of the actual correction ball. -/
29 def beta (T : H →L[ℝ] Y) (r : Y) (M : ℝ) : ℝ :=
30   Metric.infDist r (T '' Metric.closedBall 0 M)
31 
32 omit [CompleteSpace H] [CompleteSpace Y] in
33 theorem convex_budget_image (T : H →L[ℝ] Y) (M : ℝ) :
34     Convex ℝ (T '' Metric.closedBall 0 M) :=
35   (convex_closedBall (0 : H) M).linear_image T.toLinearMap
36 
37 /-- Closedness of each budget image does not assert closedness of the whole range. -/
38 theorem isClosed_budget_image (T : H →L[ℝ] Y) (M : ℝ) :
39     IsClosed (T '' Metric.closedBall 0 M) := by
40   apply IsSeqClosed.isClosed
41   intro u y hu hlim
42   choose a ha using hu
43   have hb : ∀ n, ‖a n‖ ≤ M := by
44     intro n
45     simpa only [Metric.mem_closedBall, dist_zero_right] using (ha n).1
46   have hT : Tendsto (fun n => T (a n)) atTop (𝓝 y) := by
47     simpa only [(ha _).2] using hlim
48   obtain ⟨x, hx, hnorm⟩ :=
49     BoundedApproximateRealization.exists_solution_of_bounded_approximation T a y M hb hT
50   exact ⟨x, by simpa only [Metric.mem_closedBall, dist_zero_right] using hnorm, hx⟩
51 
52 omit [CompleteSpace H] [CompleteSpace Y] in
53 theorem budget_image_nonempty (T : H →L[ℝ] Y) {M : ℝ} (hM : 0 ≤ M) :
54     (T '' Metric.closedBall 0 M).Nonempty :=
55   ⟨T 0, 0, by simpa using hM, rfl⟩
56 
57 omit [CompleteSpace H] [CompleteSpace Y] in
58 theorem beta_nonneg (T : H →L[ℝ] Y) (r : Y) (M : ℝ) : 0 ≤ beta T r M :=
59   Metric.infDist_nonneg
60 
61 omit [CompleteSpace H] [CompleteSpace Y] in
62 theorem beta_le_residual (T : H →L[ℝ] Y) (r : Y) {M : ℝ} {a : H}
63     (ha : ‖a‖ ≤ M) : beta T r M ≤ ‖r - T a‖ := by
64   exact (Metric.infDist_le_dist_of_mem
65     (show T a ∈ T '' Metric.closedBall 0 M from
66       ⟨a, by simpa only [Metric.mem_closedBall, dist_zero_right] using ha, rfl⟩)).trans_eq
67     (dist_eq_norm _ _)
68 
69 /-- Every nonnegative budget has an attaining correction, with the same budget. -/
70 theorem exists_budget_minimizer (T : H →L[ℝ] Y) (r : Y) {M : ℝ}
71     (hM : 0 ≤ M) : ∃ a : H, ‖a‖ ≤ M ∧ ‖r - T a‖ = beta T r M := by
72   obtain ⟨y, ⟨a, ha, rfl⟩, hy⟩ := exists_norm_eq_iInf_of_complete_convex
73     (budget_image_nonempty T hM) (isClosed_budget_image T M).isComplete
74     (convex_budget_image T M) r
75   refine ⟨a, by simpa only [Metric.mem_closedBall, dist_zero_right] using ha, ?_⟩
76   simpa only [beta, Metric.infDist_eq_iInf, dist_eq_norm] using hy
77 
78 /-- The distance definition equals the printed infimum over feasible corrections. -/
79 theorem beta_eq_iInf (T : H →L[ℝ] Y) (r : Y) {M : ℝ} (hM : 0 ≤ M) :
80     beta T r M = ⨅ a : {a : H // ‖a‖ ≤ M}, ‖r - T a‖ := by
81   let : Nonempty {a : H // ‖a‖ ≤ M} := ⟨⟨0, by simpa using hM⟩⟩
82   apply le_antisymm
83   · exact le_ciInf fun a => beta_le_residual T r a.2
84   · obtain ⟨a, ha, he⟩ := exists_budget_minimizer T r hM
85     exact (ciInf_le (show BddBelow (Set.range
86       (fun a : {a : H // ‖a‖ ≤ M} => ‖r - T a‖)) from
87       ⟨0, by rintro _ ⟨a, rfl⟩; exact norm_nonneg _⟩) ⟨a, ha⟩).trans_eq he
88 
89 /-- The subspace determining the unrestricted residual floor. -/
90 def rangeClosure (T : H →L[ℝ] Y) : Submodule ℝ Y :=
91   T.range.topologicalClosure
92 
93 omit [CompleteSpace H] [CompleteSpace Y] in
94 theorem rangeClosure_coe (T : H →L[ℝ] Y) :
95     (rangeClosure T : Set Y) = closure (Set.range T) := rfl
96 
97 instance rangeClosure_completeSpace (T : H →L[ℝ] Y) : CompleteSpace (rangeClosure T) :=
98   (T.range.isClosed_topologicalClosure).completeSpace_coe
99 
100 /-- Projection onto the closure of the range, not onto an assumed closed range. -/
101 def projectedDatum (T : H →L[ℝ] Y) (r : Y) : Y :=
102   (rangeClosure T).starProjection r
103 
104 omit [CompleteSpace H] in
105 theorem projectedDatum_mem (T : H →L[ℝ] Y) (r : Y) :
106     projectedDatum T r ∈ rangeClosure T :=
107   (rangeClosure T).starProjection_apply_mem r
108 
109 omit [CompleteSpace H] [CompleteSpace Y] in
110 theorem apply_mem_rangeClosure (T : H →L[ℝ] Y) (a : H) :
111     T a ∈ rangeClosure T :=
112   subset_closure (Set.mem_range_self a)
113 
114 omit [CompleteSpace H] in
115 theorem residual_sq_decomposition (T : H →L[ℝ] Y) (r : Y) (a : H) :
116     ‖r - T a‖ ^ 2 = ‖r - projectedDatum T r‖ ^ 2 +
117       ‖projectedDatum T r - T a‖ ^ 2 := by
118   have horth : inner ℝ (r - projectedDatum T r) (projectedDatum T r - T a) = 0 :=
119     (rangeClosure T).starProjection_inner_eq_zero r _
120       ((rangeClosure T).sub_mem (projectedDatum_mem T r) (apply_mem_rangeClosure T a))
121   have he := norm_add_sq_real (r - projectedDatum T r) (projectedDatum T r - T a)
122   rw [sub_add_sub_cancel, horth] at he
123   linarith
124 
125 omit [CompleteSpace H] in
126 theorem projected_residual_eq_infDist (T : H →L[ℝ] Y) (r : Y) :
127     ‖r - projectedDatum T r‖ = Metric.infDist r (closure (Set.range T)) := by
128   change ‖r - (rangeClosure T).starProjection r‖ = Metric.infDist r (rangeClosure T : Set Y)
129   simp only [Metric.infDist_eq_iInf, dist_eq_norm]
130   change ‖r - (rangeClosure T).starProjection r‖ =
131     ⨅ y : rangeClosure T, ‖r - (y : Y)‖
132   exact Submodule.starProjection_minimal r
133 
134 omit [CompleteSpace H] in
135 theorem floor_le_beta (T : H →L[ℝ] Y) (r : Y) {M : ℝ} (hM : 0 ≤ M) :
136     ‖r - projectedDatum T r‖ ≤ beta T r M := by
137   rw [projected_residual_eq_infDist]
138   exact Metric.infDist_le_infDist_of_subset
139     (by rintro _ ⟨a, _, rfl⟩; exact subset_closure (Set.mem_range_self a))
140     (budget_image_nonempty T hM)
141 
142 /-- The residual floor is reached at a finite budget exactly when the projected
143 datum is attained within that same budget. -/
144 theorem beta_eq_floor_iff (T : H →L[ℝ] Y) (r : Y) {M : ℝ} (hM : 0 ≤ M) :
145     beta T r M = ‖r - projectedDatum T r‖ ↔
146       ∃ a : H, T a = projectedDatum T r ∧ ‖a‖ ≤ M := by
147   constructor
148   · intro h
149     obtain ⟨a, ha, he⟩ := exists_budget_minimizer T r hM
150     have hsq := residual_sq_decomposition T r a
151     rw [he, h] at hsq
152     have hz : ‖projectedDatum T r - T a‖ = 0 := by nlinarith [norm_nonneg (projectedDatum T r - T a)]
153     exact ⟨a, (sub_eq_zero.mp (norm_eq_zero.mp hz)).symm, ha⟩
154   · rintro ⟨a, ha, hnorm⟩
155     apply le_antisymm _ (floor_le_beta T r hM)
156     simpa only [ha] using beta_le_residual T r hnorm
157 
158 /-- Zero residual at a fixed budget is exact feasibility, even for nonclosed range. -/
159 theorem beta_eq_zero_iff (T : H →L[ℝ] Y) (r : Y) {M : ℝ} (hM : 0 ≤ M) :
160     beta T r M = 0 ↔ ∃ a : H, T a = r ∧ ‖a‖ ≤ M := by
161   constructor
162   · intro h
163     obtain ⟨a, ha, he⟩ := exists_budget_minimizer T r hM
164     exact ⟨a, (sub_eq_zero.mp (norm_eq_zero.mp (he.trans h))).symm, ha⟩
165   · rintro ⟨a, ha, hnorm⟩
166     apply le_antisymm _ (beta_nonneg T r M)
167     simpa only [ha, sub_self, norm_zero] using beta_le_residual T r hnorm
168 
169 omit [CompleteSpace H] in
170 /-- As real budgets tend to infinity, the profile tends to distance from the
171 closure of the range. No closed-range assumption is used. -/
172 theorem beta_tendsto_infDist (T : H →L[ℝ] Y) (r : Y) :
173     Tendsto (beta T r) atTop (𝓝 (Metric.infDist r (closure (Set.range T)))) := by
174   apply Metric.tendsto_nhds.mpr
175   intro ε hε
176   have hlt : Metric.infDist r (Set.range T) <
177       Metric.infDist r (closure (Set.range T)) + ε := by
178     rw [Metric.infDist_closure]
179     exact lt_add_of_pos_right _ hε
180   obtain ⟨_, ⟨a, rfl⟩, ha⟩ :=
181     (Metric.infDist_lt_iff (Set.range_nonempty T)).mp hlt
182   filter_upwards [Filter.eventually_ge_atTop ‖a‖] with M hM
183   have hl : Metric.infDist r (closure (Set.range T)) ≤ beta T r M := by
184     rw [← projected_residual_eq_infDist]
185     exact floor_le_beta T r ((norm_nonneg a).trans hM)
186   have hu := beta_le_residual T r hM
187   rw [dist_eq_norm] at ha
188   rw [Real.dist_eq, abs_of_nonneg (sub_nonneg.mpr hl)]
189   linarith
190 
191 omit [CompleteSpace H] in
192 theorem beta_tendsto_floor (T : H →L[ℝ] Y) (r : Y) :
193     Tendsto (beta T r) atTop (𝓝 ‖r - projectedDatum T r‖) := by
194   rw [projected_residual_eq_infDist]
195   exact beta_tendsto_infDist T r
196 
197 end KomorebiSpace.BudgetProfile

Back to source controls