Exact source: MathlibAnnex/Analysis/Convex/LexicographicSelection.lean
Pinned GitHub source · Raw UTF-8 source
Back to Equal Plücker bodies yield matching generators with an almost-isometric representative
1import Mathlib23/-!4# Lexicographic selection from compact generators56A nonempty compact set is repeatedly cut down to the maximizers of a finite7ordered dictionary of continuous linear functionals. Equality of the original8convex hulls is preserved at every stage. If the dictionary separates points,9the final compact slices are singletons, and the two singletons coincide.1011The public finite-coordinate theorem keeps the original `Good` conclusion:12the common point belongs to both raw generator sets and satisfies every property13known on the first target-side support slice.14-/1516noncomputable section1718open Set19open TopologicalSpace2021namespace MathlibAnnex2223universe u2425variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]2627namespace NonemptyCompacts2829/-- A selected maximizer of a continuous linear functional on a nonempty compact set. -/30noncomputable def maximizer31 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) : E :=32 Classical.choose <|33 K.isCompact.exists_isMaxOn K.nonempty ℓ.continuous.continuousOn3435/-- The selected point belongs to the compact set. -/36theorem maximizer_mem37 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) :38 maximizer K ℓ ∈ (K : Set E) :=39 (Classical.choose_spec <|40 K.isCompact.exists_isMaxOn K.nonempty ℓ.continuous.continuousOn).14142/-- Every point of the compact set lies below the selected maximum. -/43theorem le_maximizer44 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ)45 {x : E} (hx : x ∈ (K : Set E)) :46 ℓ x ≤ ℓ (maximizer K ℓ) :=47 (Classical.choose_spec <|48 K.isCompact.exists_isMaxOn K.nonempty ℓ.continuous.continuousOn).2 hx4950/-- Maximum value of a continuous linear functional on a nonempty compact set. -/51noncomputable def maxValue52 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) : ℝ :=53 ℓ (maximizer K ℓ)5455/-- The points of a compact set attaining the maximum of `ℓ`. -/56def maxSlice57 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) : Set E :=58 {x ∈ (K : Set E) | ℓ x = maxValue K ℓ}5960/-- The selected maximizer belongs to the maximum slice. -/61theorem maximizer_mem_maxSlice62 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) :63 maximizer K ℓ ∈ maxSlice K ℓ := by64 exact ⟨maximizer_mem K ℓ, rfl⟩6566/-- A maximum slice is nonempty. -/67theorem maxSlice_nonempty68 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) :69 (maxSlice K ℓ).Nonempty :=70 ⟨maximizer K ℓ, maximizer_mem_maxSlice K ℓ⟩7172/-- A maximum slice is compact. -/73theorem isCompact_maxSlice74 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) :75 IsCompact (maxSlice K ℓ) := by76 have hclosed : IsClosed {x : E | ℓ x = maxValue K ℓ} :=77 isClosed_eq ℓ.continuous continuous_const78 exact K.isCompact.inter_right hclosed7980/-- Bundle the maximum slice as a nonempty compact set. -/81noncomputable def refine82 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) :83 TopologicalSpace.NonemptyCompacts E where84 carrier := maxSlice K ℓ85 isCompact' := isCompact_maxSlice K ℓ86 nonempty' := maxSlice_nonempty K ℓ8788@[simp] theorem mem_refine89 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) {x : E} :90 x ∈ (refine K ℓ : Set E) ↔ x ∈ (K : Set E) ∧ ℓ x = maxValue K ℓ :=91 Iff.rfl9293end NonemptyCompacts9495open NonemptyCompacts9697/-- The support face of the convex hull cut out by the raw maximum value. -/98def supportFace [FiniteDimensional ℝ E]99 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) : Set E :=100 {x ∈ convexHull ℝ (K : Set E) | ℓ x = maxValue K ℓ}101102/-- The convex hull of the raw maximum slice is exactly the corresponding support face. -/103theorem convexHull_maxSlice_eq_supportFace [FiniteDimensional ℝ E]104 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) :105 convexHull ℝ (maxSlice K ℓ) = supportFace K ℓ := by106 classical107 ext x108 constructor109 · intro hx110 refine ⟨convexHull_mono (fun y hy => hy.1) hx, ?_⟩111 have hlevelConvex : Convex ℝ {y : E | ℓ y = maxValue K ℓ} := by112 intro y hy z hz a b ha hb hab113 change ℓ (a • y + b • z) = maxValue K ℓ114 change ℓ y = maxValue K ℓ at hy115 change ℓ z = maxValue K ℓ at hz116 simp only [map_add, map_smul, smul_eq_mul, hy, hz]117 rw [← add_mul, hab, one_mul]118 exact convexHull_min (fun y hy => hy.2) hlevelConvex hx119 · rintro ⟨hxHull, hxLevel⟩120 rw [_root_.convexHull_eq] at hxHull ⊢121 rcases hxHull with ⟨ι, t, w, z, hw0, hw1, hz, hcenter⟩122 have hlinear : ℓ x = ∑ i ∈ t, w i * ℓ (z i) := by123 rw [← hcenter, Finset.centerMass_eq_of_sum_1 _ _ hw1]124 simp125 have hgap_nonneg :126 ∀ i ∈ t, 0 ≤ w i * (maxValue K ℓ - ℓ (z i)) := by127 intro i hi128 exact mul_nonneg (hw0 i hi)129 (sub_nonneg.mpr (le_maximizer K ℓ (hz i hi)))130 have hgap_sum :131 ∑ i ∈ t, w i * (maxValue K ℓ - ℓ (z i)) = 0 := by132 simp_rw [mul_sub]133 rw [Finset.sum_sub_distrib, ← Finset.sum_mul, hw1, one_mul]134 rw [← hlinear, hxLevel, sub_self]135 have hgap_zero :136 ∀ i ∈ t, w i * (maxValue K ℓ - ℓ (z i)) = 0 :=137 (Finset.sum_eq_zero_iff_of_nonneg hgap_nonneg).1 hgap_sum138 let t' : Finset ι := t.filter fun i => w i ≠ 0139 refine ⟨ι, t', w, z, ?_, ?_, ?_, ?_⟩140 · intro i hi141 exact hw0 i (Finset.mem_filter.1 hi).1142 · calc143 ∑ i ∈ t', w i = ∑ i ∈ t, w i := by144 apply Finset.sum_subset (Finset.filter_subset _ _)145 intro i hi hit'146 by_contra hwi147 apply hit'148 change i ∈ t.filter fun j => w j ≠ 0149 exact Finset.mem_filter.2 ⟨hi, hwi⟩150 _ = 1 := hw1151 · intro i hi152 have hit : i ∈ t := (Finset.mem_filter.1 hi).1153 have hwi : w i ≠ 0 := (Finset.mem_filter.1 hi).2154 have hprod := hgap_zero i hit155 have hgap : maxValue K ℓ - ℓ (z i) = 0 :=156 (mul_eq_zero.mp hprod).resolve_left hwi157 exact ⟨hz i hit, (sub_eq_zero.mp hgap).symm⟩158 · calc159 t'.centerMass w z = t.centerMass w z := by160 simpa [t'] using161 (Finset.centerMass_filter_ne_zero (t := t) (w := w) (z := z))162 _ = x := hcenter163164/-- Every point of the convex hull lies below the maximum on its compact generator. -/165theorem le_maxValue_of_mem_convexHull [FiniteDimensional ℝ E]166 (K : TopologicalSpace.NonemptyCompacts E) (ℓ : E →L[ℝ] ℝ) {x : E}167 (hx : x ∈ convexHull ℝ (K : Set E)) :168 ℓ x ≤ maxValue K ℓ := by169 have hhalf : Convex ℝ {y : E | ℓ y ≤ maxValue K ℓ} := by170 intro y hy z hz a b ha hb hab171 change ℓ (a • y + b • z) ≤ maxValue K ℓ172 simp only [map_add, map_smul, smul_eq_mul]173 calc174 a * ℓ y + b * ℓ z ≤ a * maxValue K ℓ + b * maxValue K ℓ :=175 add_le_add176 (mul_le_mul_of_nonneg_left hy ha)177 (mul_le_mul_of_nonneg_left hz hb)178 _ = maxValue K ℓ := by rw [← add_mul, hab, one_mul]179 exact convexHull_min (fun y hy => le_maximizer K ℓ hy) hhalf hx180181/-- Equal convex hulls give equal maximum values for every continuous linear functional. -/182theorem maxValue_eq_of_convexHull_eq [FiniteDimensional ℝ E]183 (K L : TopologicalSpace.NonemptyCompacts E)184 (hHull : convexHull ℝ (K : Set E) = convexHull ℝ (L : Set E))185 (ℓ : E →L[ℝ] ℝ) :186 maxValue K ℓ = maxValue L ℓ := by187 apply le_antisymm188 · have hx : maximizer K ℓ ∈ convexHull ℝ (L : Set E) := by189 rw [← hHull]190 exact subset_convexHull ℝ _ (maximizer_mem K ℓ)191 simpa [maxValue] using le_maxValue_of_mem_convexHull L ℓ hx192 · have hy : maximizer L ℓ ∈ convexHull ℝ (K : Set E) := by193 rw [hHull]194 exact subset_convexHull ℝ _ (maximizer_mem L ℓ)195 simpa [maxValue] using le_maxValue_of_mem_convexHull K ℓ hy196197/-- Cutting two compact generators by the same functional preserves equality of convex hulls. -/198theorem refine_convexHull_eq [FiniteDimensional ℝ E]199 (K L : TopologicalSpace.NonemptyCompacts E)200 (hHull : convexHull ℝ (K : Set E) = convexHull ℝ (L : Set E))201 (ℓ : E →L[ℝ] ℝ) :202 convexHull ℝ (refine K ℓ : Set E) =203 convexHull ℝ (refine L ℓ : Set E) := by204 change convexHull ℝ (maxSlice K ℓ) = convexHull ℝ (maxSlice L ℓ)205 rw [convexHull_maxSlice_eq_supportFace K ℓ,206 convexHull_maxSlice_eq_supportFace L ℓ]207 have hmax := maxValue_eq_of_convexHull_eq K L hHull ℓ208 ext x209 simp [supportFace, hHull, hmax]210211/-- Successive maximum refinement by an ordered finite dictionary of functionals. -/212noncomputable def lexicographicRefine :213 List (E →L[ℝ] ℝ) → TopologicalSpace.NonemptyCompacts E →214 TopologicalSpace.NonemptyCompacts E215 | [], K => K216 | ℓ :: ls, K => lexicographicRefine ls (refine K ℓ)217218/-- A full lexicographic refinement stays inside its input compact set. -/219theorem lexicographicRefine_subset220 (ls : List (E →L[ℝ] ℝ)) (K : TopologicalSpace.NonemptyCompacts E) :221 (lexicographicRefine ls K : Set E) ⊆ (K : Set E) := by222 induction ls generalizing K with223 | nil =>224 intro x hx225 exact hx226 | cons ℓ ls ih =>227 intro x hx228 have hxTail : x ∈ (lexicographicRefine ls (refine K ℓ) : Set E) := by229 simpa [lexicographicRefine] using hx230 have hxRefine : x ∈ (refine K ℓ : Set E) :=231 ih (K := refine K ℓ) hxTail232 exact ((mem_refine K ℓ).1 hxRefine).1233234/-- Survivors of the listed refinements agree under every listed functional. -/235theorem apply_eq_of_mem_lexicographicRefine236 (ls : List (E →L[ℝ] ℝ)) (K : TopologicalSpace.NonemptyCompacts E)237 {x y : E}238 (hx : x ∈ (lexicographicRefine ls K : Set E))239 (hy : y ∈ (lexicographicRefine ls K : Set E)) :240 ∀ ℓ ∈ ls, ℓ x = ℓ y := by241 induction ls generalizing K x y with242 | nil =>243 intro ℓ hℓ244 simp at hℓ245 | cons ℓ ls ih =>246 intro φ hφ247 have hxTail : x ∈ (lexicographicRefine ls (refine K ℓ) : Set E) := by248 simpa [lexicographicRefine] using hx249 have hyTail : y ∈ (lexicographicRefine ls (refine K ℓ) : Set E) := by250 simpa [lexicographicRefine] using hy251 have hxRefine : x ∈ (refine K ℓ : Set E) :=252 lexicographicRefine_subset ls (refine K ℓ) hxTail253 have hyRefine : y ∈ (refine K ℓ : Set E) :=254 lexicographicRefine_subset ls (refine K ℓ) hyTail255 rcases List.mem_cons.mp hφ with hφℓ | hφTail256 · subst φ257 exact ((mem_refine K ℓ).1 hxRefine).2.trans258 ((mem_refine K ℓ).1 hyRefine).2.symm259 · exact ih (K := refine K ℓ) hxTail hyTail φ hφTail260261/-- A point-separating dictionary leaves at most one survivor. -/262theorem lexicographicRefine_subsingleton263 (ls : List (E →L[ℝ] ℝ))264 (hsep : ∀ x y : E, (∀ ℓ ∈ ls, ℓ x = ℓ y) → x = y)265 (K : TopologicalSpace.NonemptyCompacts E) :266 (lexicographicRefine ls K : Set E).Subsingleton := by267 intro x hx y hy268 exact hsep x y (apply_eq_of_mem_lexicographicRefine ls K hx hy)269270/-- Repeated lexicographic refinement preserves equality of convex hulls. -/271theorem lexicographicRefine_convexHull_eq [FiniteDimensional ℝ E]272 (ls : List (E →L[ℝ] ℝ))273 (K L : TopologicalSpace.NonemptyCompacts E)274 (hHull : convexHull ℝ (K : Set E) = convexHull ℝ (L : Set E)) :275 convexHull ℝ (lexicographicRefine ls K : Set E) =276 convexHull ℝ (lexicographicRefine ls L : Set E) := by277 induction ls generalizing K L with278 | nil =>279 simpa [lexicographicRefine] using hHull280 | cons ℓ ls ih =>281 simp only [lexicographicRefine]282 exact ih283 (K := refine K ℓ)284 (L := refine L ℓ)285 (refine_convexHull_eq K L hHull ℓ)286287/-- A common raw generator selected by a finite point-separating dictionary.288289The conclusion deliberately retains `Good z`; this theorem is not merely an290intersection statement. -/291theorem exists_common_of_convexHull_eq [FiniteDimensional ℝ E]292 (ls : List (E →L[ℝ] ℝ))293 (hsep : ∀ x y : E, (∀ ℓ ∈ ls, ℓ x = ℓ y) → x = y)294 (K L : TopologicalSpace.NonemptyCompacts E)295 (hHull : convexHull ℝ (K : Set E) = convexHull ℝ (L : Set E))296 (ℓ : E →L[ℝ] ℝ)297 (Good : E → Prop)298 (hgood : ∀ z ∈ maxSlice L ℓ, Good z) :299 ∃ z, z ∈ (K : Set E) ∧ z ∈ (L : Set E) ∧ Good z := by300 have hSliceHull :301 convexHull ℝ (refine K ℓ : Set E) =302 convexHull ℝ (refine L ℓ : Set E) :=303 refine_convexHull_eq K L hHull ℓ304 have hFinalHull :305 convexHull ℝ (lexicographicRefine ls (refine K ℓ) : Set E) =306 convexHull ℝ (lexicographicRefine ls (refine L ℓ) : Set E) :=307 lexicographicRefine_convexHull_eq ls (refine K ℓ) (refine L ℓ) hSliceHull308 rcases (lexicographicRefine ls (refine K ℓ)).nonempty with ⟨x, hx⟩309 rcases (lexicographicRefine ls (refine L ℓ)).nonempty with ⟨y, hy⟩310 have hsubL :311 (lexicographicRefine ls (refine L ℓ) : Set E).Subsingleton :=312 lexicographicRefine_subsingleton ls hsep (refine L ℓ)313 have hLsingleton :314 (lexicographicRefine ls (refine L ℓ) : Set E) = {y} :=315 hsubL.eq_singleton_of_mem hy316 have hxHullL :317 x ∈ convexHull ℝ (lexicographicRefine ls (refine L ℓ) : Set E) := by318 rw [← hFinalHull]319 exact subset_convexHull ℝ _ hx320 have hxy : x = y := by321 rw [hLsingleton, convexHull_singleton] at hxHullL322 simpa using hxHullL323 have hxK0 : x ∈ (refine K ℓ : Set E) :=324 lexicographicRefine_subset ls (refine K ℓ) hx325 have hyL0 : y ∈ (refine L ℓ : Set E) :=326 lexicographicRefine_subset ls (refine L ℓ) hy327 have hxL0 : x ∈ (refine L ℓ : Set E) := by328 simpa [hxy] using hyL0329 have hxK : x ∈ (K : Set E) := ((mem_refine K ℓ).1 hxK0).1330 have hxL : x ∈ (L : Set E) := ((mem_refine L ℓ).1 hxL0).1331 have hxSlice : x ∈ maxSlice L ℓ := by332 exact (mem_refine L ℓ).1 hxL0333 exact ⟨x, hxK, hxL, hgood x hxSlice⟩334335/-- Coordinate projection on a finite real Pi space. -/336noncomputable def coordinate {ι : Type*} [Fintype ι] (i : ι) :337 (ι → ℝ) →L[ℝ] ℝ :=338 ContinuousLinearMap.proj i339340/-- Every coordinate projection, in a fixed finite enumeration. -/341noncomputable def allCoordinates {ι : Type*} [Fintype ι] :342 List ((ι → ℝ) →L[ℝ] ℝ) := by343 classical344 exact Finset.univ.toList.map (fun i : ι => coordinate i)345346@[simp] theorem coordinate_mem_allCoordinates {ι : Type*} [Fintype ι]347 (i : ι) :348 coordinate i ∈ (allCoordinates : List ((ι → ℝ) →L[ℝ] ℝ)) := by349 classical350 simp [allCoordinates]351352/-- All coordinate projections separate points of a finite real Pi space. -/353theorem allCoordinates_separate {ι : Type*} [Fintype ι]354 (x y : ι → ℝ)355 (h : ∀ ℓ ∈ (allCoordinates : List ((ι → ℝ) →L[ℝ] ℝ)), ℓ x = ℓ y) :356 x = y := by357 funext i358 have hi := h (coordinate i) (coordinate_mem_allCoordinates i)359 simpa [coordinate] using hi360361/-- Finite-coordinate common-generator extraction with the full `Good` conclusion. -/362theorem exists_common_pi {ι : Type*} [Fintype ι]363 (K L : TopologicalSpace.NonemptyCompacts (ι → ℝ))364 (hHull : convexHull ℝ (K : Set (ι → ℝ)) =365 convexHull ℝ (L : Set (ι → ℝ)))366 (ℓ : (ι → ℝ) →L[ℝ] ℝ)367 (Good : (ι → ℝ) → Prop)368 (hgood : ∀ z ∈ maxSlice L ℓ, Good z) :369 ∃ z, z ∈ (K : Set (ι → ℝ)) ∧ z ∈ (L : Set (ι → ℝ)) ∧ Good z := by370 exact exists_common_of_convexHull_eq371 (allCoordinates : List ((ι → ℝ) →L[ℝ] ℝ))372 allCoordinates_separate K L hHull ℓ Good hgood373374end MathlibAnnex