NestedMinimumCorrections.lean

1 import Mathlib.Analysis.InnerProductSpace.Projection.Minimal
2 import Mathlib.Analysis.Convex.Basic
3 import Mathlib.Topology.Order.MonotoneConvergence
4 import Mathlib.Tactic
5 
6 /-!
7 # Nested minimum corrections (WR02)
8 
9 Minimum norm points are constructed from nonempty closed convex sets in an arbitrary
10 real Hilbert space. A general convex projection inequality proves a strong nested
11 intersection theorem. For affine sets the inequality becomes the exact WR02 energy
12 identity. No finite dimensionality, separability, or compactness of norm balls is
13 assumed.
14 -/
15 
16 open Filter Set
17 open scoped Topology
18 
19 namespace KomorebiSpace.NestedMinimumCorrections
20 
21 variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
22 
23 /-- Membership and global minimum norm, rather than an assumed projection operator. -/
24 def IsMinimum (C : Set H) (a : H) : Prop :=
25   a ∈ C ∧ ∀ x ∈ C, ‖a‖ ≤ ‖x‖
26 
27 /-- Existence uses the Hilbert projection theorem on the actual closed convex set. -/
28 theorem exists_minimum (C : Set H) (hne : C.Nonempty) (hc : IsClosed C)
29     (hcv : Convex ℝ C) : ∃ a, IsMinimum C a := by
30   obtain ⟨a, ha, he⟩ := exists_norm_eq_iInf_of_complete_convex hne hc.isComplete hcv (0 : H)
31   refine ⟨a, ha, ?_⟩
32   intro x hx
33   have hi := ciInf_le (show BddBelow (Set.range (fun w : C => ‖(0 : H) - w‖)) from
34     ⟨0, by rintro _ ⟨w, rfl⟩; exact norm_nonneg _⟩) (⟨x, hx⟩ : C)
35   simpa only [zero_sub, norm_neg] using he.le.trans hi
36 
37 omit [CompleteSpace H] in
38 /-- The normal variational inequality of the minimum norm point. -/
39 theorem minimum_inner_nonneg {C : Set H} (hcv : Convex ℝ C) {a : H}
40     (ha : IsMinimum C a) {x : H} (hx : x ∈ C) :
41     0 ≤ inner ℝ a (x - a) := by
42   let : Nonempty C := ⟨⟨a, ha.1⟩⟩
43   have he : ‖(0 : H) - a‖ = ⨅ w : C, ‖(0 : H) - w‖ := by
44     apply le_antisymm
45     · apply le_ciInf
46       intro w
47       simpa only [zero_sub, norm_neg] using ha.2 w w.2
48     · exact ciInf_le (show BddBelow (Set.range (fun w : C => ‖(0 : H) - w‖)) from
49         ⟨0, by rintro _ ⟨w, rfl⟩; exact norm_nonneg _⟩) (⟨a, ha.1⟩ : C)
50   have hi := (norm_eq_iInf_iff_real_inner_le_zero hcv ha.1).mp he x hx
51   simpa only [zero_sub, inner_neg_left, neg_nonpos] using hi
52 
53 omit [CompleteSpace H] in
54 /-- The convex projection inequality controls distance by the difference of energies. -/
55 theorem minimum_energy_le {C : Set H} (hcv : Convex ℝ C) {a : H}
56     (ha : IsMinimum C a) {x : H} (hx : x ∈ C) :
57     ‖x - a‖ ^ 2 ≤ ‖x‖ ^ 2 - ‖a‖ ^ 2 := by
58   have hi := minimum_inner_nonneg hcv ha hx
59   have he := norm_add_sq_real a (x - a)
60   rw [add_sub_cancel] at he
61   nlinarith
62 
63 omit [CompleteSpace H] in
64 /-- The minimizer is unique, including in the zero dimensional case. -/
65 theorem minimum_unique {C : Set H} (hcv : Convex ℝ C) {a b : H}
66     (ha : IsMinimum C a) (hb : IsMinimum C b) : a = b := by
67   have he := minimum_energy_le hcv ha hb.1
68   have hn := ha.2 b hb.1
69   have hn' := hb.2 a ha.1
70   rw [le_antisymm hn' hn] at he
71   have hz : ‖b - a‖ = 0 := by nlinarith [sq_nonneg ‖b - a‖, norm_nonneg (b - a)]
72   exact (sub_eq_zero.mp (norm_eq_zero.mp hz)).symm
73 
74 /-- A canonical choice is independent of the existence proof by uniqueness. -/
75 noncomputable def minimumPoint (C : Set H) (hne : C.Nonempty) (hc : IsClosed C)
76     (hcv : Convex ℝ C) : H := Classical.choose (exists_minimum C hne hc hcv)
77 
78 theorem minimumPoint_spec (C : Set H) (hne : C.Nonempty) (hc : IsClosed C)
79     (hcv : Convex ℝ C) : IsMinimum C (minimumPoint C hne hc hcv) :=
80   Classical.choose_spec (exists_minimum C hne hc hcv)
81 
82 omit [InnerProductSpace ℝ H] [CompleteSpace H] in
83 /-- Bounded energies with the nested projection inequality force a norm Cauchy sequence. -/
84 theorem cauchySeq_of_energy_le (a : ℕ → H)
85     (he : ∀ n m, n ≤ m → ‖a m - a n‖ ^ 2 ≤ ‖a m‖ ^ 2 - ‖a n‖ ^ 2)
86     (hb : ∃ M : ℝ, ∀ n, ‖a n‖ ≤ M) : CauchySeq a := by
87   obtain ⟨M, hM⟩ := hb
88   have hM0 : 0 ≤ M := (norm_nonneg (a 0)).trans (hM 0)
89   have hbd : BddAbove (Set.range (fun n => ‖a n‖ ^ 2)) := by
90     refine ⟨M ^ 2, ?_⟩
91     rintro _ ⟨n, rfl⟩
92     exact pow_le_pow_left₀ (norm_nonneg _) (hM n) 2
93   apply Metric.cauchySeq_iff'.mpr
94   intro ε hε
95   obtain ⟨q, ⟨N, rfl⟩, hN⟩ := exists_lt_of_lt_csSup
96     (Set.range_nonempty (fun n => ‖a n‖ ^ 2))
97     (show sSup (Set.range (fun n => ‖a n‖ ^ 2)) - ε ^ 2 <
98       sSup (Set.range (fun n => ‖a n‖ ^ 2)) by nlinarith)
99   refine ⟨N, ?_⟩
100   intro n hn
101   have hnS := le_csSup hbd (Set.mem_range_self n)
102   have hd := he N n hn
103   rw [dist_eq_norm]
104   nlinarith [norm_nonneg (a n - a N)]
105 
106 /-- The actual minimum sequence of closed convex nested sets converges if uniformly bounded. -/
107 theorem minimum_sequence_converges (C : ℕ → Set H)
108     (hc : ∀ n, IsClosed (C n)) (hcv : ∀ n, Convex ℝ (C n)) (hnest : Antitone C)
109     (a : ℕ → H) (ha : ∀ n, IsMinimum (C n) (a n))
110     (hb : ∃ M : ℝ, ∀ n, ‖a n‖ ≤ M) :
111     ∃ aStar, Tendsto a atTop (𝓝 aStar) ∧ IsMinimum (⋂ n, C n) aStar := by
112   have hca : CauchySeq a := cauchySeq_of_energy_le a
113     (fun n m hnm => minimum_energy_le (hcv n) (ha n) (hnest hnm (ha m).1)) hb
114   obtain ⟨aStar, ht⟩ := cauchySeq_tendsto_of_complete hca
115   have hm : aStar ∈ ⋂ n, C n := by
116     apply Set.mem_iInter.mpr
117     intro n
118     apply (hc n).mem_of_tendsto ht
119     filter_upwards [Filter.eventually_ge_atTop n] with m hm
120     exact hnest hm (ha m).1
121   refine ⟨aStar, ht, hm, ?_⟩
122   intro x hx
123   exact le_of_tendsto ht.norm (Filter.Eventually.of_forall (fun n =>
124     (ha n).2 x (Set.mem_iInter.mp hx n)))
125 
126 /-- General convex intersection bridge: bounded feasible representatives suffice.
127 This is stronger than the affine existence part of WR02 and supports WR01. -/
128 theorem exists_mem_iInter_of_closed_convex_bounded (C : ℕ → Set H)
129     (hne : ∀ n, (C n).Nonempty) (hc : ∀ n, IsClosed (C n))
130     (hcv : ∀ n, Convex ℝ (C n)) (hnest : Antitone C)
131     (M : ℝ) (hbudget : ∀ n, ∃ a ∈ C n, ‖a‖ ≤ M) :
132     ∃ a, (∀ n, a ∈ C n) ∧ ‖a‖ ≤ M := by
133   let a : ℕ → H := fun n => minimumPoint (C n) (hne n) (hc n) (hcv n)
134   have ha : ∀ n, IsMinimum (C n) (a n) := fun n =>
135     minimumPoint_spec (C n) (hne n) (hc n) (hcv n)
136   have hb : ∀ n, ‖a n‖ ≤ M := by
137     intro n
138     obtain ⟨x, hx, hMx⟩ := hbudget n
139     exact ((ha n).2 x hx).trans hMx
140   obtain ⟨aStar, ht, hm⟩ := minimum_sequence_converges C hc hcv hnest a ha ⟨M, hb⟩
141   exact ⟨aStar, Set.mem_iInter.mp hm.1,
142     le_of_tendsto ht.norm (Filter.Eventually.of_forall hb)⟩
143 
144 omit [CompleteSpace H] in
145 /-- Affineness upgrades the convex variational inequality to orthogonality. -/
146 theorem affine_minimum_inner_eq_zero (A : AffineSubspace ℝ H) {a : H}
147     (ha : IsMinimum (A : Set H) a) {x : H} (hx : x ∈ A) :
148     inner ℝ a (x - a) = 0 := by
149   have hp := minimum_inner_nonneg A.convex ha hx
150   have hr : -(x - a) + a ∈ A := by
151     simpa only [vsub_eq_sub, vadd_eq_add, neg_one_smul] using
152       A.smul_vsub_vadd_mem (-1 : ℝ) hx ha.1 ha.1
153   have hn := minimum_inner_nonneg A.convex ha hr
154   have hid : -(x - a) + a - a = -(x - a) := by abel
155   rw [hid, inner_neg_right] at hn
156   linarith
157 
158 omit [CompleteSpace H] in
159 /-- The exact affine energy identity applies to every point in the same affine set. -/
160 theorem affine_minimum_energy (A : AffineSubspace ℝ H) {a : H}
161     (ha : IsMinimum (A : Set H) a) {x : H} (hx : x ∈ A) :
162     ‖x - a‖ ^ 2 = ‖x‖ ^ 2 - ‖a‖ ^ 2 := by
163   have hi := affine_minimum_inner_eq_zero A ha hx
164   have he := norm_add_sq_real a (x - a)
165   rw [add_sub_cancel, hi] at he
166   linarith
167 
168 /-- Canonically constructed minimum corrections for a sequence of affine constraints. -/
169 noncomputable def affineCorrections (A : ℕ → AffineSubspace ℝ H)
170     (hne : ∀ n, (A n : Set H).Nonempty) (hc : ∀ n, IsClosed (A n : Set H)) : ℕ → H :=
171   fun n => minimumPoint (A n : Set H) (hne n) (hc n) (A n).convex
172 
173 theorem affineCorrections_spec (A : ℕ → AffineSubspace ℝ H)
174     (hne : ∀ n, (A n : Set H).Nonempty) (hc : ∀ n, IsClosed (A n : Set H)) (n : ℕ) :
175     IsMinimum (A n : Set H) (affineCorrections A hne hc n) :=
176   minimumPoint_spec (A n : Set H) (hne n) (hc n) (A n).convex
177 
178 /-- WR02 finite energy equality for all ordered index pairs. -/
179 theorem nested_affine_energy (A : ℕ → AffineSubspace ℝ H)
180     (hne : ∀ n, (A n : Set H).Nonempty) (hc : ∀ n, IsClosed (A n : Set H))
181     (hnest : Antitone A) {n m : ℕ} (hnm : n ≤ m) :
182     ‖affineCorrections A hne hc m - affineCorrections A hne hc n‖ ^ 2 =
183       ‖affineCorrections A hne hc m‖ ^ 2 - ‖affineCorrections A hne hc n‖ ^ 2 :=
184   affine_minimum_energy (A n) (affineCorrections_spec A hne hc n)
185     (hnest hnm (affineCorrections_spec A hne hc m).1)
186 
187 /-- WR02: the minimum correction norms are nondecreasing. -/
188 theorem nested_affine_norm_monotone (A : ℕ → AffineSubspace ℝ H)
189     (hne : ∀ n, (A n : Set H).Nonempty) (hc : ∀ n, IsClosed (A n : Set H))
190     (hnest : Antitone A) : Monotone (fun n => ‖affineCorrections A hne hc n‖) := by
191   intro n m hnm
192   exact (affineCorrections_spec A hne hc n).2 _
193     (hnest hnm (affineCorrections_spec A hne hc m).1)
194 
195 /-- WR02: nonempty intersection is equivalent to a finite uniform minimum budget. -/
196 theorem nested_affine_intersection_iff_bounded (A : ℕ → AffineSubspace ℝ H)
197     (hne : ∀ n, (A n : Set H).Nonempty) (hc : ∀ n, IsClosed (A n : Set H))
198     (hnest : Antitone A) :
199     (∃ x, ∀ n, x ∈ A n) ↔ ∃ M : ℝ, ∀ n, ‖affineCorrections A hne hc n‖ ≤ M := by
200   constructor
201   · rintro ⟨x, hx⟩
202     exact ⟨‖x‖, fun n => (affineCorrections_spec A hne hc n).2 x (hx n)⟩
203   · rintro ⟨M, hM⟩
204     obtain ⟨x, hx, _⟩ := exists_mem_iInter_of_closed_convex_bounded
205       (fun n => (A n : Set H)) hne hc (fun n => (A n).convex) hnest M
206       (fun n => ⟨affineCorrections A hne hc n, (affineCorrections_spec A hne hc n).1, hM n⟩)
207     exact ⟨x, hx⟩
208 
209 /-- WR02: the minimum corrections converge strongly to the unique minimum in the
210 intersection, and the exact error is the remaining energy. -/
211 theorem nested_affine_strong_realization (A : ℕ → AffineSubspace ℝ H)
212     (hne : ∀ n, (A n : Set H).Nonempty) (hc : ∀ n, IsClosed (A n : Set H))
213     (hnest : Antitone A) (hb : ∃ M : ℝ, ∀ n, ‖affineCorrections A hne hc n‖ ≤ M) :
214     ∃ aStar, Tendsto (affineCorrections A hne hc) atTop (𝓝 aStar) ∧
215       IsMinimum (⋂ n, (A n : Set H)) aStar ∧
216       (∀ b, IsMinimum (⋂ n, (A n : Set H)) b → b = aStar) ∧
217       ∀ n, ‖aStar - affineCorrections A hne hc n‖ ^ 2 =
218         ‖aStar‖ ^ 2 - ‖affineCorrections A hne hc n‖ ^ 2 := by
219   obtain ⟨aStar, ht, hm⟩ := minimum_sequence_converges
220     (fun n => (A n : Set H)) hc (fun n => (A n).convex) hnest
221     (affineCorrections A hne hc) (affineCorrections_spec A hne hc) hb
222   refine ⟨aStar, ht, hm, ?_, ?_⟩
223   · intro b hb
224     exact minimum_unique (convex_iInter (fun n => (A n).convex)) hb hm
225   · intro n
226     exact affine_minimum_energy (A n) (affineCorrections_spec A hne hc n)
227       (Set.mem_iInter.mp hm.1 n)
228 
229 /-- WR02: an empty intersection forces the entire norm sequence to infinity. -/
230 theorem nested_affine_escape (A : ℕ → AffineSubspace ℝ H)
231     (hne : ∀ n, (A n : Set H).Nonempty) (hc : ∀ n, IsClosed (A n : Set H))
232     (hnest : Antitone A) (hempty : ¬ ∃ x, ∀ n, x ∈ A n) :
233     Tendsto (fun n => ‖affineCorrections A hne hc n‖) atTop atTop := by
234   apply tendsto_atTop_atTop_of_monotone' (nested_affine_norm_monotone A hne hc hnest)
235   intro hb
236   apply hempty
237   apply (nested_affine_intersection_iff_bounded A hne hc hnest).mpr
238   obtain ⟨M, hM⟩ := hb
239   exact ⟨M, fun n => hM (Set.mem_range_self n)⟩
240 
241 end KomorebiSpace.NestedMinimumCorrections

Back to source controls