Exact source: MathlibAnnex/Analysis/Convex/CompactHull.lean
Pinned GitHub source · Raw UTF-8 source
Back to The convex hull of a compact set in a finite real coordinate space
1import Mathlib23/-!4# Compact convex hulls in finite real coordinate spaces56This file proves compactness of the convex hull of a compact subset of a finite7real Pi space. Mathlib supplies the finite-set theorem and the finite8Carathéodory representation; the remaining compact-parameter argument is kept9here as the actual Annex delta.10-/1112noncomputable section1314open Set Finset15open scoped BigOperators1617namespace MathlibAnnex1819/-- Coefficients and points for a convex combination with exactly `k` slots. -/20private def fixedConvexCarrier {ι : Type*} [Fintype ι]21 (s : Set (ι → ℝ)) (k : ℕ) :22 Set ((Fin k → ℝ) × (Fin k → ι → ℝ)) :=23 (stdSimplex ℝ (Fin k)) ×ˢ (Set.univ.pi fun _ : Fin k => s)2425/-- Evaluation of a fixed-length convex combination. -/26private def fixedConvexEval {ι : Type*} [Fintype ι] {k : ℕ}27 (q : (Fin k → ℝ) × (Fin k → ι → ℝ)) : ι → ℝ :=28 ∑ i, q.1 i • q.2 i2930/-- The set of all convex combinations with exactly `k` slots. -/31private def fixedConvexImage {ι : Type*} [Fintype ι]32 (s : Set (ι → ℝ)) (k : ℕ) : Set (ι → ℝ) :=33 fixedConvexEval '' fixedConvexCarrier s k3435private theorem isCompact_fixedConvexCarrier {ι : Type*} [Fintype ι]36 {s : Set (ι → ℝ)} (hs : IsCompact s) (k : ℕ) :37 IsCompact (fixedConvexCarrier s k) := by38 have hw : IsCompact (stdSimplex ℝ (Fin k)) :=39 isCompact_stdSimplex ℝ (Fin k)40 have hz : IsCompact (Set.univ.pi fun _ : Fin k => s) := by41 exact isCompact_univ_pi (fun _ => hs)42 exact hw.prod hz4344private theorem continuous_fixedConvexEval {ι : Type*} [Fintype ι] {k : ℕ} :45 Continuous (fixedConvexEval :46 ((Fin k → ℝ) × (Fin k → ι → ℝ)) → (ι → ℝ)) := by47 unfold fixedConvexEval48 fun_prop4950private theorem isCompact_fixedConvexImage {ι : Type*} [Fintype ι]51 {s : Set (ι → ℝ)} (hs : IsCompact s) (k : ℕ) :52 IsCompact (fixedConvexImage s k) := by53 exact (isCompact_fixedConvexCarrier hs k).image continuous_fixedConvexEval5455private theorem affineIndependent_card_le_pi_succ {ι κ : Type*}56 [Fintype ι] [Fintype κ] {z : κ → ι → ℝ}57 (hz : AffineIndependent ℝ z) :58 Fintype.card κ ≤ Fintype.card ι + 1 := by59 classical60 cases isEmpty_or_nonempty κ with61 | inl hκ => simp62 | inr hκ =>63 let i0 : κ := Classical.choice hκ64 have hlin :=65 (affineIndependent_iff_linearIndependent_vsub ℝ z i0).1 hz66 have hcard : Fintype.card {i : κ // i ≠ i0} ≤ Fintype.card ι := by67 exact (Pi.basisFun ℝ ι).card_le_card_of_linearIndependent hlin68 have hsubcard :69 Fintype.card {i : κ // i ≠ i0} = Fintype.card κ - 1 := by70 calc71 Fintype.card {i : κ // i ≠ i0} =72 Fintype.card κ - Fintype.card {i : κ // i = i0} :=73 Fintype.card_subtype_compl (fun i : κ => i = i0)74 _ = Fintype.card κ - 1 := by75 rw [Fintype.card_subtype_eq i0]76 have hκcard_pos : 0 < Fintype.card κ :=77 Fintype.card_pos_iff.mpr hκ78 omega7980private theorem exists_bounded_convex_representation {ι : Type*} [Fintype ι]81 {s : Set (ι → ℝ)} {x : ι → ℝ} (hx : x ∈ convexHull ℝ s) :82 ∃ k : Fin (Fintype.card ι + 2), x ∈ fixedConvexImage s k.1 := by83 classical84 rcases eq_pos_convex_span_of_mem_convexHull hx with85 ⟨κ, hκ, z, w, hz, hind, hwpos, hwsum, hvalue⟩86 letI : Fintype κ := hκ87 have hk : Fintype.card κ < Fintype.card ι + 2 := by88 have := affineIndependent_card_le_pi_succ hind89 omega90 let k : Fin (Fintype.card ι + 2) := ⟨Fintype.card κ, hk⟩91 let e : κ ≃ Fin (Fintype.card κ) := Fintype.equivFin κ92 let w' : Fin k.1 → ℝ := fun j => w (e.symm j)93 let z' : Fin k.1 → ι → ℝ := fun j => z (e.symm j)94 refine ⟨k, ⟨(w', z'), ?_, ?_⟩⟩95 · constructor96 · change (∀ j : Fin k.1, 0 ≤ w' j) ∧ ∑ j, w' j = 197 refine ⟨fun j => (hwpos (e.symm j)).le, ?_⟩98 have hsum :99 (∑ j : Fin (Fintype.card κ), w (e.symm j)) = ∑ i : κ, w i :=100 Equiv.sum_comp e.symm w101 simpa [k, w'] using hsum.trans hwsum102 · intro j hj103 exact hz ⟨e.symm j, rfl⟩104 · change ∑ j : Fin k.1, w' j • z' j = x105 calc106 (∑ j : Fin k.1, w' j • z' j) = ∑ i : κ, w i • z i := by107 have hsum :108 (∑ j : Fin (Fintype.card κ), w (e.symm j) • z (e.symm j)) =109 ∑ i : κ, w i • z i :=110 Equiv.sum_comp e.symm (fun i : κ => w i • z i)111 simpa [k, w', z'] using hsum112 _ = x := hvalue113114private theorem fixedConvexImage_subset_convexHull {ι : Type*} [Fintype ι]115 (s : Set (ι → ℝ)) (k : ℕ) :116 fixedConvexImage s k ⊆ convexHull ℝ s := by117 rintro x ⟨q, hq, rfl⟩118 rcases hq with ⟨hw, hz⟩119 have hc := convex_convexHull ℝ s120 change (∀ i, 0 ≤ q.1 i) ∧ ∑ i, q.1 i = 1 at hw121 have hmem := hc.sum_mem (t := Finset.univ) (w := q.1) (z := q.2)122 (fun i _ => hw.1 i)123 (by simpa using hw.2)124 (fun i _ => subset_convexHull ℝ s (hz i (mem_univ i)))125 simpa [fixedConvexEval] using hmem126127private theorem convexHull_eq_iUnion_fixedConvexImage {ι : Type*} [Fintype ι]128 (s : Set (ι → ℝ)) :129 convexHull ℝ s =130 ⋃ k : Fin (Fintype.card ι + 2), fixedConvexImage s k.1 := by131 apply Set.Subset.antisymm132 · intro x hx133 rcases exists_bounded_convex_representation hx with ⟨k, hk⟩134 exact mem_iUnion.2 ⟨k, hk⟩135 · exact iUnion_subset fun k => fixedConvexImage_subset_convexHull s k.1136137/-- The convex hull of a compact subset of a finite real Pi space is compact. -/138theorem isCompact_convexHull_pi {ι : Type*} [Fintype ι]139 (s : Set (ι → ℝ)) (hs : IsCompact s) :140 IsCompact (convexHull ℝ s) := by141 rw [convexHull_eq_iUnion_fixedConvexImage]142 exact isCompact_iUnion fun k => isCompact_fixedConvexImage hs k.1143144end MathlibAnnex