Convex Analysis (Rockafellar, 1970) -- Chapter 04 -- Section 17 -- Part 8

open scoped BigOperators Pointwiseopen Topologyopen Filtersection Chap04section Section17

Corollary 17.1.6. Let be any function (modeled here as together with the side condition ∀ (x : ?m.1), sorry ≠ ⊥ : Prop∀ x, Unknown identifier `f`f x ≠ ⊥). Let Unknown identifier `k`k be the positively homogeneous convex function generated by Unknown identifier `f`f (equivalently, generated by conv sorry : Set (Fin ?m.1 → ℝ)conv Unknown identifier `f`f, modeled here as convexHullFunction sorry : (Fin ?m.1 → ℝ) → ERealconvexHullFunction Unknown identifier `f`f).

Then, for each vector Unknown identifier `x`sorry ≠ 0 : Propx ≠ 0, , where the infimum is taken over all expressions of Unknown identifier `x`x as a nonnegative linear combination of at most Unknown identifier `n`sorry + 1 : ℕn+1 vectors (allowing zero coefficients to pad the representation).

theorem positivelyHomogeneousConvexFunctionGenerated_convexHullFunction_eq_sInf_nonnegLinearCombination {n : Nat} {f : (Fin n → Real) → EReal} (h_not_bot : ∀ x, f x ≠ (⊥ : EReal)) : ∀ x : Fin n → Real, x ≠ 0 → positivelyHomogeneousConvexFunctionGenerated (convexHullFunction f) x = sInf { z : EReal | ∃ (x' : Fin (n + 1) → Fin n → Real) (c : Fin (n + 1) → Real), (∀ i, 0 ≤ c i) ∧ (∑ i, c i • x' i = x) ∧ z = ∑ i, ((c i : Real) : EReal) * f (x' i) } := by classical intro x hx by_cases hfinite : ∃ x0, f x0 ≠ (⊤ : EReal) · have hpos : positivelyHomogeneousConvexFunctionGenerated (convexHullFunction f) x = sInf { z : EReal | ∃ lam : Real, 0 < lam ∧ z = rightScalarMultiple (convexHullFunction f) lam x } := by have hconv : ConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) (convexHullFunction f) := by simpa using (convexHullFunction_greatest_convex_minorant (g := f)).1 have hfinite' : ∃ x, convexHullFunction f x ≠ (⊤ : EReal) := by rcases hfinite with ⟨x0, hx0⟩ rcases (convexHullFunction_greatest_convex_minorant (g := f)) with ⟨_hconv, hle, -⟩ refine ⟨x0, ?_⟩ intro htop have htop_le : (⊤ : EReal) ≤ f x0 := by simpa [htop] using hle x0 have htop_eq : f x0 = (⊤ : EReal) := (top_le_iff).1 htop_le exact hx0 htop_eq have hmain := (infimumRepresentation_posHomogeneousHull (n := n) (h := convexHullFunction f) hconv hfinite').2 have hmain' := hmain x (Or.inl hx) simpa using hmain' have hstep1 := sInf_pos_rightScalarMultiple_convexHullFunction_eq_sInf_exists_scaled_convexCombination_add_one (f := f) (h_not_bot := h_not_bot) (x := x) have hstep2 := scaled_convexCombination_add_one_witness_iff_nonneg_coeff_witness (f := f) (x := x) hx have hstep2' : sInf { z : EReal | ∃ lam : Real, 0 < lam ∧ ∃ (x' : Fin (n + 1) → Fin n → Real) (w : Fin (n + 1) → Real), IsConvexWeights (n + 1) w ∧ x = ∑ i, (lam * w i) • x' i ∧ z = ∑ i, ((lam * w i : Real) : EReal) * f (x' i) } = sInf { z : EReal | ∃ (x' : Fin (n + 1) → Fin n → Real) (c : Fin (n + 1) → Real), (∀ i, 0 ≤ c i) ∧ (∑ i, c i • x' i = x) ∧ z = ∑ i, ((c i : Real) : EReal) * f (x' i) } := by simpa [eq_comm] using hstep2 exact hpos.trans (hstep1.trans hstep2') · have htop : ∀ x, f x = (⊤ : EReal) := by intro x0 by_contra hx0 exact hfinite ⟨x0, hx0⟩ have hconv_top : ConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) (fun _ : Fin n → Real => (⊤ : EReal)) := by have hE : epigraph (Set.univ : Set (Fin n → Real)) (fun _ : Fin n → Real => (⊤ : EReal)) = (∅ : Set ((Fin n → Real) × Real)) := by ext p constructor · intro hp rcases hp with ⟨-, hp⟩ have htop' : (p.2 : EReal) = ⊤ := (top_le_iff).1 hp exact (EReal.coe_ne_top _ htop').elim · intro hp cases hp have hconv_empty : Convex ℝ (∅ : Set ((Fin n → Real) × Real)) := by simpa using (convex_empty : Convex ℝ (∅ : Set ((Fin n → Real) × Real))) simpa [ConvexFunctionOn, hE] using hconv_empty have hle_top : (fun _ : Fin n → Real => (⊤ : EReal)) ≤ f := by intro x0 simp [htop x0] have hle_conv : (fun _ : Fin n → Real => (⊤ : EReal)) ≤ convexHullFunction f := (convexHullFunction_greatest_convex_minorant (g := f)).2.2 (fun _ => (⊤ : EReal)) hconv_top hle_top have hconvHull_top : ∀ y, convexHullFunction f y = (⊤ : EReal) := by intro y have htop_y : (⊤ : EReal) ≤ convexHullFunction f y := by simpa using hle_conv y exact (top_le_iff).1 htop_y have hepigraph_empty : epigraph (Set.univ : Set (Fin n → Real)) (convexHullFunction f) = (∅ : Set ((Fin n → Real) × Real)) := by ext p constructor · intro hp rcases hp with ⟨-, hp⟩ have htop' : (p.2 : EReal) = ⊤ := by have hp' : (⊤ : EReal) ≤ p.2 := by convert hp using 1; simp [hconvHull_top p.1] exact (top_le_iff).1 hp' exact (EReal.coe_ne_top _ htop').elim · intro hp cases hp have hconv : ConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) (convexHullFunction f) := by simpa using (convexHullFunction_greatest_convex_minorant (g := f)).1 have hempty : { μ : ℝ | (x, μ) ∈ convexConeGeneratedEpigraph (convexHullFunction f) } = ∅ := by ext μ constructor · intro hmem have hmem' := (mem_convexConeGeneratedEpigraph_iff (h := convexHullFunction f) hconv).1 hmem rcases hmem' with hzero | ⟨lam, hlam, hmem'⟩ · have hx0 : x = 0 := by simpa using congrArg Prod.fst hzero exact (hx hx0).elim · have hmem'' : (x, μ) ∈ (∅ : Set ((Fin n → Real) × Real)) := by convert hmem' using 1; simp [hepigraph_empty] exact hmem''.elim · intro hmem cases hmem have hleft : positivelyHomogeneousConvexFunctionGenerated (convexHullFunction f) x = ⊤ := by simp [positivelyHomogeneousConvexFunctionGenerated, hempty] have hright : sInf { z : EReal | ∃ (x' : Fin (n + 1) → Fin n → Real) (c : Fin (n + 1) → Real), (∀ i, 0 ≤ c i) ∧ (∑ i, c i • x' i = x) ∧ z = ∑ i, ((c i : Real) : EReal) * f (x' i) } = ⊤ := by refine le_antisymm ?_ ?_ · exact le_top · refine le_sInf ?_ intro z hz rcases hz with ⟨x', c, hc, hxsum, hz⟩ have hpos : ∃ i, 0 < c i := by by_contra hpos have hzero : ∀ i, c i = 0 := by intro i have hle : c i ≤ 0 := le_of_not_gt ((not_exists.mp hpos) i) exact le_antisymm hle (hc i) have hx0 : x = 0 := by simpa [hzero] using hxsum.symm exact (hx hx0).elim rcases hpos with ⟨i0, hi0⟩ have hterm_top : ((c i0 : Real) : EReal) * f (x' i0) = ⊤ := by have hposE : (0 : EReal) < (c i0 : EReal) := (EReal.coe_pos).2 hi0 simpa [htop (x' i0)] using (EReal.mul_top_of_pos (x := (c i0 : EReal)) hposE) have hsum_top : (∑ i, ((c i : Real) : EReal) * f (x' i)) = ⊤ := by have hsum := (Finset.add_sum_erase (s := Finset.univ) (f := fun i => ((c i : Real) : EReal) * f (x' i)) (a := i0) (h := by simp)) calc (∑ i, ((c i : Real) : EReal) * f (x' i)) = ((c i0 : Real) : EReal) * f (x' i0) + (Finset.univ.erase i0).sum (fun i => ((c i : Real) : EReal) * f (x' i)) := by simpa using hsum.symm _ = ⊤ := by have hsum_ne_bot : (Finset.univ.erase i0).sum (fun i => ((c i : Real) : EReal) * f (x' i)) ≠ ⊥ := by refine sum_ne_bot_of_ne_bot (s := Finset.univ.erase i0) (f := fun i => ((c i : Real) : EReal) * f (x' i)) ?_ intro i hi have hne_bot : f (x' i) ≠ ⊥ := h_not_bot (x' i) refine (EReal.mul_ne_bot ((c i : Real) : EReal) (f (x' i))).2 ?_ refine ⟨?_, ?_, ?_, ?_⟩ · left exact EReal.coe_ne_bot _ · right exact hne_bot · left exact EReal.coe_ne_top _ · left exact (EReal.coe_nonneg).2 (hc i) simpa [hterm_top] using (EReal.top_add_of_ne_bot hsum_ne_bot) have hz' : z = ⊤ := by simp [hz, hsum_top] simp [hz'] simp [hleft, hright]

Linear independence of the lifted points (1, sorry) : ℕ × ?m.2(1, Unknown identifier `p`p i) from affine independence of Unknown identifier `p`p.

lemma linearIndependent_lift1_of_affineIndependent {n d : Nat} {p : Fin (d + 1) → Fin n → ℝ} (hp : AffineIndependent ℝ p) : LinearIndependent ℝ (fun i => (Fin.cases (1 : ℝ) (p i) : Fin (n + 1) → ℝ)) := by classical let lift1 : (Fin n → ℝ) → Fin (n + 1) → ℝ := fun x => Fin.cases (1 : ℝ) x have hp' := (affineIndependent_iff (k := ℝ) (p := p)).1 hp refine (linearIndependent_iff' (R := ℝ) (v := fun i => lift1 (p i))).2 ?_ intro s g hsum have hsum0' : (∑ i ∈ s, g i • lift1 (p i)) 0 = 0 := by simpa using congrArg (fun v => v 0) hsum have hsum0 : s.sum g = 0 := by simp [lift1] at hsum0' simpa using hsum0' have hsumP : ∑ i ∈ s, g i • p i = 0 := by ext j have hsumj : (∑ i ∈ s, g i • lift1 (p i)) (Fin.succ j) = 0 := by simpa using congrArg (fun v => v (Fin.succ j)) hsum simp [lift1] at hsumj simpa using hsumj exact hp' s g hsum0 hsumP

Convex hull of affinely independent vertices is a generalized simplex.

lemma isGeneralizedSimplex_conv_range_of_affineIndependent {n d : Nat} {p : Fin (d + 1) → Fin n → ℝ} (hp : AffineIndependent ℝ p) : IsGeneralizedSimplex n d (conv (Set.range p)) := by classical let lift1 : (Fin n → ℝ) → Fin (n + 1) → ℝ := fun x => Fin.cases (1 : ℝ) x let v : Fin (d + 1) → Fin (n + 1) → ℝ := fun i => lift1 (p i) let f_lin : (Fin (d + 1) → ℝ) →ₗ[ℝ] (Fin (n + 1) → ℝ) := Fintype.linearCombination ℝ v let f : (Fin (d + 1) → ℝ) →ᵃ[ℝ] (Fin (n + 1) → ℝ) := f_lin.toAffineMap let O : Set (Fin (n + 1) → ℝ) := f '' nonnegOrthant (d + 1) refine ⟨O, ?_, ?_⟩ · have hlin : LinearIndependent ℝ v := linearIndependent_lift1_of_affineIndependent (p := p) hp have hf_inj : Function.Injective f := by have hlin_inj : Function.Injective f_lin := (LinearIndependent.fintypeLinearCombination_injective (v := v) hlin) simpa [f, f_lin] using hlin_inj exact ⟨f, hf_inj, rfl⟩ · ext x constructor · intro hx -- use affine combination representation rcases (by simpa [convexHull_range_eq_exists_affineCombination (R := ℝ) (v := p)] using hx) with ⟨s, w, hw_nonneg, hw_sum, hx_aff⟩ let c : Fin (d + 1) → ℝ := fun i => if i ∈ s then w i else 0 have hc_nonneg : ∀ i, 0 ≤ c i := by intro i by_cases hi : i ∈ s · simp [c, hi, hw_nonneg i hi] · simp [c, hi] have hsum_c : ∑ i, c i = 1 := by have hsum' : ∑ i, c i = ∑ i ∈ s, w i := by calc ∑ i, c i = ∑ i, if i ∈ s then w i else 0 := by simp [c] _ = ∑ i ∈ s, w i := Fintype.sum_ite_mem s w have hsum'' : ∑ i ∈ s, w i = 1 := by simpa using hw_sum exact hsum'.trans hsum'' have hx_sum : ∑ i, c i • p i = x := by have hx_aff' : ∑ i ∈ s, w i • p i = x := by have hsum'' : s.sum w = 1 := hw_sum calc ∑ i ∈ s, w i • p i = (Finset.affineCombination ℝ s p) w := by symm exact (Finset.affineCombination_eq_linear_combination (k := ℝ) (s := s) (p := p) (w := w) (by simpa using hsum'')) _ = x := hx_aff have hx_sum' : ∑ i, c i • p i = ∑ i ∈ s, w i • p i := by calc ∑ i, c i • p i = ∑ i, if i ∈ s then w i • p i else 0 := by simp [c] _ = ∑ i ∈ s, w i • p i := Fintype.sum_ite_mem s (fun i => w i • p i) exact hx_sum'.trans hx_aff' -- show lift1 x in O ∩ liftingHyperplane refine ⟨?memO, ?memH⟩ · refine ⟨c, ?_, ?_⟩ · change ∀ i, 0 ≤ c i exact hc_nonneg · -- f c = lift1 x ext i cases i using Fin.cases with | zero => -- coordinate 0: sum of weights simp [f, f_lin, v, lift1, Fintype.linearCombination_apply, hsum_c] | succ j => have hx_sum' := congrArg (fun v => v j) hx_sum have hsucc : (f c) (Fin.succ j) = (∑ i, c i • p i) j := by simp [f, f_lin, v, lift1, Fintype.linearCombination_apply] simpa [hsucc, lift1] using hx_sum' · -- lift1 x is always in the lifting hyperplane simp [liftingHyperplane_eq] · intro hx rcases hx with ⟨hxO, _hxH⟩ rcases hxO with ⟨c, hc, hc_eq⟩ have hc_nonneg : ∀ i, 0 ≤ c i := by simpa [nonnegOrthant] using hc -- compute sum weights from coordinate 0 have hsum_c : ∑ i, c i = 1 := by have h0 : (f c) 0 = 1 := by have h0' : (f c) 0 = (lift1 x) 0 := by simpa using congrArg (fun v => v 0) hc_eq simpa [lift1] using h0' simpa [f, f_lin, v, lift1, Fintype.linearCombination_apply] using h0 -- compute x as combination have hx_sum : ∑ i, c i • p i = x := by ext j have hsj : (f c) (Fin.succ j) = (lift1 x) (Fin.succ j) := by simpa using congrArg (fun v => v (Fin.succ j)) hc_eq simp [f, f_lin, v, lift1, Fintype.linearCombination_apply] at hsj simpa [lift1] using hsj -- conclude membership in convex hull refine mem_convexHull_of_exists_fintype (ι := Fin (d + 1)) (s := Set.range p) (w := c) (z := p) ?_ ?_ ?_ ?_ · exact hc_nonneg · exact hsum_c · intro i; exact ⟨i, rfl⟩ · exact hx_sum

For any Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `C`C, there are Unknown identifier `d`sorry + 1 : ℕd+1 affinely independent points of Unknown identifier `C`C with Unknown identifier `x`x as the first vertex, where Unknown identifier `d`d is the finrank of the direction of affineSpan ℝ sorry : AffineSubspace ℝ ?m.2affineSpan ℝ Unknown identifier `C`C.

lemma exists_affineIndependent_vertices_through_point_finrank_direction {n : Nat} {C : Set (Fin n → ℝ)} {x : Fin n → ℝ} (hx : x ∈ C) : let d := Module.finrank ℝ (affineSpan ℝ C).direction ∃ p : Fin (d + 1) → Fin n → ℝ, p 0 = x ∧ (∀ i, p i ∈ C) ∧ AffineIndependent ℝ p := by classical intro d let s : Set (Fin n → ℝ) := (fun y => y -ᵥ x) '' C have hdir : (affineSpan ℝ C).direction = Submodule.span ℝ s := by simpa [direction_affineSpan] using (vectorSpan_eq_span_vsub_set_right (k := ℝ) (s := C) (p := x) hx) -- equality of finranks have hfinrank : Module.finrank ℝ ↥(Submodule.span ℝ s) = Module.finrank ℝ ↥(affineSpan ℝ C).direction := by have hlin : ↥(Submodule.span ℝ s) ≃ₗ[ℝ] ↥(affineSpan ℝ C).direction := LinearEquiv.ofEq (Submodule.span ℝ s) (affineSpan ℝ C).direction hdir.symm simpa using (LinearEquiv.finrank_eq hlin) -- choose a spanning linearly independent family of vsub vectors obtain ⟨f, hfmem, _hfspan, hlin⟩ := (Submodule.exists_fun_fin_finrank_span_eq (K := ℝ) s) -- reindex to `Fin d` let g : Fin d → Fin n → ℝ := fun i => f (Fin.cast hfinrank.symm i) have hgmem : ∀ i, g i ∈ s := by intro i simpa [g] using hfmem (Fin.cast hfinrank.symm i) have hlin_g : LinearIndependent ℝ g := hlin.comp (Fin.cast hfinrank.symm) (Fin.cast_injective _) -- pick points in C whose differences are g have hmem : ∀ i, ∃ y ∈ C, g i = y -ᵥ x := by intro i rcases hgmem i with ⟨y, hyC, hy⟩ exact ⟨y, hyC, hy.symm⟩ choose q hqC hqeq using hmem -- build the vertex family let p : Fin (d + 1) → Fin n → ℝ := Fin.cases x q have hp0 : p 0 = x := by simp [p] have hpC : ∀ i, p i ∈ C := by intro i cases i using Fin.cases with | zero => simpa [p] using hx | succ i => simpa [p] using hqC i -- affine independence let e : Fin d ≃ {i : Fin (d + 1) // i ≠ 0} := { toFun := fun i => ⟨Fin.succ i, by simp⟩ invFun := fun i => Fin.pred i.1 i.2 left_inv := by intro i simp right_inv := by intro i ext simp [Fin.succ_pred] } have hlin_sub : LinearIndependent ℝ ((fun i : {i : Fin (d + 1) // i ≠ 0} => p i -ᵥ p 0) ∘ e) := by -- reduce to g simpa [e, p, g, hqeq] using hlin_g have hlin_vsub : LinearIndependent ℝ (fun i : {i : Fin (d + 1) // i ≠ 0} => p i -ᵥ p 0) := (linearIndependent_equiv e).1 hlin_sub have haff : AffineIndependent ℝ p := (affineIndependent_iff_linearIndependent_vsub (k := ℝ) (p := p) (i1 := (0 : Fin (d + 1)))).2 hlin_vsub exact ⟨p, hp0, hpC, haff⟩

Theorem 17.1 (Caratheodory's Theorem), union-of-simplices formulation. With and (here ), the set Unknown identifier `C`C is the union of all generalized Unknown identifier `d`d-dimensional simplices contained in Unknown identifier `C`C.

theorem mixedConvexHull_eq_sUnion_generalizedSimplex_finrank_affineSpan_direction {n : Nat} (S₀ S₁ : Set (Fin n → Real)) : (let C := mixedConvexHull (n := n) S₀ S₁ let d := Module.finrank Real (affineSpan Real C).direction C = ⋃₀ {T : Set (Fin n → Real) | IsGeneralizedSimplex n d T ∧ T ⊆ C}) := by classical intro C d ext x constructor · intro hx -- choose an affinely independent simplex through x rcases (exists_affineIndependent_vertices_through_point_finrank_direction (C := C) (x := x) hx) with ⟨p, hp0, hpC, hpAI⟩ let T : Set (Fin n → Real) := conv (Set.range p) have hxT : x ∈ T := by have hxrange : x ∈ Set.range p := by exact ⟨0, hp0⟩ exact (subset_convexHull ℝ (Set.range p)) hxrange have hsubset : T ⊆ C := by have hsubset_range : Set.range p ⊆ C := by intro y hy rcases hy with ⟨i, rfl⟩ exact hpC i exact convexHull_min hsubset_range (convex_mixedConvexHull (n := n) S₀ S₁) have hT_simplex : IsGeneralizedSimplex n d T := by -- use affinely independent vertices dsimp [T] exact isGeneralizedSimplex_conv_range_of_affineIndependent (p := p) hpAI refine Set.mem_sUnion.mpr ?_ refine ⟨T, ?_, hxT⟩ exact ⟨hT_simplex, hsubset⟩ · intro hx rcases Set.mem_sUnion.mp hx with ⟨T, hT, hxT⟩ rcases hT with ⟨_hT_simplex, hsubset⟩ exact hsubset hxT
private def cor1717_xAxis : Set (Fin 2 → Real) := {x | x 1 = 0}private def cor1717_p : Fin 2 → Real := ![0, 1]private def cor1717_q (k : Nat) : Fin 2 → Real := ![(k + 1 : Real), 0]private noncomputable def cor1717_z (k : Nat) : Fin 2 → Real := (1 - (1 / (k + 1 : Real))) • cor1717_p + (1 / (k + 1 : Real)) • cor1717_q kprivate def cor1717_lim : Fin 2 → Real := ![1, 1]

The x-axis union the point (0, 1) : ℕ × ℕ(0,1) is closed in Fin 2 → ℝ : TypeFin 2 → ℝ.

lemma cor1717_isClosed_xAxis_union_point : IsClosed (cor1717_xAxis ∪ {cor1717_p}) := by have hxAxis : IsClosed cor1717_xAxis := by have hcont : Continuous (fun x : Fin 2 → Real => x 1) := continuous_apply 1 have hconst : Continuous (fun _ : Fin 2 → Real => (0 : Real)) := continuous_const simpa [cor1717_xAxis] using (isClosed_eq hcont hconst) simpa using hxAxis.union (isClosed_singleton : IsClosed ({cor1717_p} : Set (Fin 2 → Real)))

The explicit convex-combination sequence lies in the convex hull.

lemma cor1717_zSeq_mem_conv : ∀ k, cor1717_z k ∈ conv (cor1717_xAxis ∪ {cor1717_p}) := by classical intro k have ht_nonneg : 0 ≤ (1 / (k + 1 : Real)) := by have hkpos : (0 : Real) < (k + 1 : Real) := by exact_mod_cast (Nat.succ_pos k) exact le_of_lt (one_div_pos.mpr hkpos) have ht_le : (1 / (k + 1 : Real)) ≤ 1 := by have hle : (1 : Real) ≤ (k + 1 : Real) := by exact_mod_cast (Nat.succ_le_succ (Nat.zero_le k)) have ha : (0 : Real) < (1 : Real) := by norm_num simpa using (one_div_le_one_div_of_le ha hle) have ha : 0 ≤ (1 - (1 / (k + 1 : Real))) := sub_nonneg.mpr ht_le have hab : (1 - (1 / (k + 1 : Real))) + (1 / (k + 1 : Real)) = 1 := by ring have hz : cor1717_z k ∈ convexHull ℝ (cor1717_xAxis ∪ {cor1717_p}) := by refine (mem_convexHull_iff_exists_fin_isConvexCombination 2 (cor1717_xAxis ∪ {cor1717_p}) (cor1717_z k)).2 ?_ refine ⟨2, (fun i : Fin 2 => if i = 0 then cor1717_p else cor1717_q k), ?_, ?_⟩ · intro i fin_cases i <;> simp [cor1717_xAxis, cor1717_p, cor1717_q] · have hcomb : IsConvexCombination 2 2 (fun i : Fin 2 => if i = 0 then cor1717_p else cor1717_q k) ((1 - (1 / (k + 1 : Real))) • cor1717_p + (1 / (k + 1 : Real)) • cor1717_q k) := isConvexCombination_two 2 cor1717_p (cor1717_q k) (1 - (1 / (k + 1 : Real))) (1 / (k + 1 : Real)) ha ht_nonneg hab simpa [cor1717_z] using hcomb simpa [conv] using hz

The explicit sequence converges to (1, 1) : ℕ × ℕ(1,1).

lemma cor1717_tendsto_zSeq : Tendsto cor1717_z atTop (𝓝 cor1717_lim) := by refine tendsto_pi_nhds.2 ?_ intro i fin_cases i · have hconst : Tendsto (fun _ : Nat => (1 : Real)) atTop (𝓝 (1 : Real)) := tendsto_const_nhds have h0 : (fun k : Nat => cor1717_z k 0) = fun _ => (1 : Real) := by funext k have hk : (k + 1 : Real) ≠ 0 := by exact_mod_cast (Nat.succ_ne_zero k) simp [cor1717_z, cor1717_p, cor1717_q, hk] simp [cor1717_lim, h0] · have hdiv : Tendsto (fun k : Nat => (1 : Real) / ((k : Real) + 1)) atTop (𝓝 (0 : Real)) := by simpa using (tendsto_one_div_add_atTop_nhds_zero_nat : Tendsto (fun k : Nat => (1 : Real) / ((k : Real) + 1)) atTop (𝓝 (0 : Real))) have hdiv' : Tendsto (fun k : Nat => (1 : Real) / (k + 1 : Real)) atTop (𝓝 (0 : Real)) := by simpa using hdiv have hconst : Tendsto (fun _ : Nat => (1 : Real)) atTop (𝓝 (1 : Real)) := tendsto_const_nhds have hsub : Tendsto (fun k : Nat => (1 : Real) - (1 : Real) / (k + 1 : Real)) atTop (𝓝 (1 - 0)) := hconst.sub hdiv' simpa [cor1717_z, cor1717_p, cor1717_q, cor1717_lim] using hsub

The limit point (1, 1) : ℕ × ℕ(1,1) is not in the convex hull of the x-axis union (0, 1) : ℕ × ℕ(0,1).

lemma cor1717_limit_not_mem_conv : cor1717_lim ∉ conv (cor1717_xAxis ∪ {cor1717_p}) := by classical intro hmem have hmem' : cor1717_lim ∈ convexHull ℝ (cor1717_xAxis ∪ {cor1717_p}) := by simpa [conv] using hmem rcases (mem_convexHull_iff_exists_fin_isConvexCombination 2 (cor1717_xAxis ∪ {cor1717_p}) cor1717_lim).1 hmem' with ⟨m, x, hxS, hcomb⟩ rcases hcomb with ⟨w, hw0, hw1, hsum⟩ have hsum1 : (∑ i, w i * x i 1) = (1 : Real) := by have hsum1' : (1 : Real) = ∑ i, w i * x i 1 := by simpa [cor1717_lim, Finset.sum_apply, smul_eq_mul] using (congrArg (fun v : Fin 2 → Real => v 1) hsum) exact hsum1'.symm have hx01 : ∀ i, x i 1 = 0 ∨ x i 1 = 1 := by intro i rcases hxS i with hxS' | hxS' · left simpa [cor1717_xAxis] using hxS' · right have hx' : x i = cor1717_p := by simpa using hxS' simpa [cor1717_p] using congrArg (fun v : Fin 2 → Real => v 1) hx' have hnonneg : ∀ i, 0 ≤ w i * (1 - x i 1) := by intro i have hxle : 0 ≤ 1 - x i 1 := by rcases hx01 i with h0 | h1 · simp [h0] · simp [h1] exact mul_nonneg (hw0 i) hxle have hsum0 : (∑ i, w i * (1 - x i 1)) = 0 := by calc ∑ i, w i * (1 - x i 1) = (∑ i, w i) - ∑ i, w i * x i 1 := by simp [mul_sub, Finset.sum_sub_distrib, mul_one] _ = 0 := by simp [hw1, hsum1] have hterm_zero : ∀ i, w i * (1 - x i 1) = 0 := by have hnonneg' : ∀ i ∈ (Finset.univ : Finset (Fin m)), 0 ≤ w i * (1 - x i 1) := by intro i _ exact hnonneg i have hterm_zero' := (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin m))) (f := fun i => w i * (1 - x i 1)) hnonneg').1 (by simpa using hsum0) intro i exact hterm_zero' i (by simp) have hw_zero_of_axis : ∀ i, x i 1 = 0 → w i = 0 := by intro i h0 have hterm := hterm_zero i simpa [h0] using hterm have hx_eq_p : ∀ i, x i 1 = 1 → x i = cor1717_p := by intro i h1 rcases hxS i with hxS' | hxS' · have h0 : x i 1 = 0 := by simpa [cor1717_xAxis] using hxS' exfalso exact one_ne_zero (h1.symm.trans h0) · simpa [cor1717_p] using hxS' have hterm_eq : ∀ i, w i • x i = w i • cor1717_p := by intro i rcases hx01 i with h0 | h1 · have hw : w i = 0 := hw_zero_of_axis i h0 simp [hw] · have hx : x i = cor1717_p := hx_eq_p i h1 simp [hx] have hsum_eq_p : ∑ i, w i • x i = cor1717_p := by calc ∑ i, w i • x i = ∑ i, w i • cor1717_p := by classical refine Finset.sum_congr rfl ?_ intro i _ exact hterm_eq i _ = (∑ i, w i) • cor1717_p := by simpa using (Finset.sum_smul (s := (Finset.univ : Finset (Fin m))) (f := w) (x := cor1717_p)).symm _ = cor1717_p := by simp [hw1] have hlim_eq : cor1717_lim = cor1717_p := by calc cor1717_lim = ∑ i, w i • x i := hsum _ = cor1717_p := hsum_eq_p have h0 := congrArg (fun v : Fin 2 → Real => v 0) hlim_eq simp [cor1717_lim, cor1717_p] at h0

Crollary 17.1.7 (Convex hull of a closed set need not be closed), LaTeX label .

In general, the convex hull of a closed subset of need not be closed. In particular, if is the union of a line and a single point not on that line, then is not closed.

theorem exists_isClosed_set_conv_not_isClosed : ∃ (n : Nat) (S : Set (Fin n → Real)), IsClosed S ∧ ¬ IsClosed (conv S) := by classical refine ⟨2, cor1717_xAxis ∪ {cor1717_p}, ?_, ?_⟩ · simpa using cor1717_isClosed_xAxis_union_point · intro hclosed have hzmem : ∀ k, cor1717_z k ∈ conv (cor1717_xAxis ∪ {cor1717_p}) := cor1717_zSeq_mem_conv have hzlim : Tendsto cor1717_z atTop (𝓝 cor1717_lim) := cor1717_tendsto_zSeq have hlimmem : cor1717_lim ∈ conv (cor1717_xAxis ∪ {cor1717_p}) := hclosed.mem_of_tendsto hzlim (Filter.Eventually.of_forall hzmem) exact cor1717_limit_not_mem_conv hlimmem

The convex hull of the x-axis union (0, 1) : ℕ × ℕ(0,1) is not closed.

lemma cor1717_not_isClosed_conv_xAxis_union_point : ¬ IsClosed (conv (cor1717_xAxis ∪ {cor1717_p})) := by intro hclosed have hzmem : ∀ k, cor1717_z k ∈ conv (cor1717_xAxis ∪ {cor1717_p}) := cor1717_zSeq_mem_conv have hzlim : Tendsto cor1717_z atTop (𝓝 cor1717_lim) := cor1717_tendsto_zSeq have hlimmem : cor1717_lim ∈ conv (cor1717_xAxis ∪ {cor1717_p}) := hclosed.mem_of_tendsto hzlim (Filter.Eventually.of_forall hzmem) exact cor1717_limit_not_mem_conv hlimmem

An affine equivalence sending an affine line to the x-axis and a point off the line to (0, 1) : ℕ × ℕ(0,1).

lemma exists_affineEquiv_image_line_eq_xAxis_and_map_point {L : AffineSubspace Real (Fin 2 → Real)} {p : Fin 2 → Real} (hL : Module.finrank Real L.direction = 1) (hp : p ∉ (L : Set (Fin 2 → Real))) : ∃ e : (Fin 2 → Real) ≃ᵃ[Real] (Fin 2 → Real), e '' (L : Set (Fin 2 → Real)) = cor1717_xAxis ∧ e p = cor1717_p := by classical have hLne : L ≠ ⊥ := by intro hbot have hdim : Module.finrank Real L.direction = 0 := by simp [hbot, AffineSubspace.direction_bot] rw [hL] at hdim exact (Nat.succ_ne_zero 0) hdim rcases (AffineSubspace.nonempty_iff_ne_bot L).2 hLne with ⟨x0, hx0L⟩ have hdir_ne_bot : (L.direction : Submodule Real (Fin 2 → Real)) ≠ ⊥ := by intro hbot have hdim : Module.finrank Real L.direction = 0 := by simp [hbot] rw [hL] at hdim exact (Nat.succ_ne_zero 0) hdim rcases (Submodule.ne_bot_iff _).1 hdir_ne_bot with ⟨v, hvdir, hv0⟩ let w : Fin 2 → Real := p -ᵥ x0 have hw0 : w ≠ 0 := by intro hw0 have hpL : p ∈ (L : Set (Fin 2 → Real)) := by have hp_eq : p = x0 := by simpa [w] using (vsub_eq_zero_iff_eq.1 hw0) simpa [hp_eq] using hx0L exact hp hpL have hw_not_dir : w ∉ L.direction := by intro hw have hpL : p ∈ (L : Set (Fin 2 → Real)) := by have hw' := (AffineSubspace.vadd_mem_iff_mem_direction (s := L) w hx0L).2 hw simpa [w, vsub_vadd] using hw' exact hp hpL let f : Fin 2 → Fin 2 → Real := fun i => if i = 0 then v else w have hlin : LinearIndependent Real f := by refine (linearIndependent_fin2 (K := Real) (V := Fin 2 → Real) (f := f)).2 ?_ refine ⟨?_, ?_⟩ · simpa [f] using hw0 · intro a by_cases ha : a = 0 · simpa [f, ha, eq_comm] using hv0 · intro h have hw' : w = (a⁻¹ : Real) • v := by calc w = (a⁻¹ : Real) • (a • w) := by simpa using (inv_smul_smul₀ ha w).symm _ = (a⁻¹ : Real) • v := by simpa [f] using congrArg (fun z => (a⁻¹ : Real) • z) h have hwdir : w ∈ L.direction := by simpa [hw'] using (L.direction.smul_mem (a⁻¹) hvdir) exact (hw_not_dir hwdir).elim have hspan_finrank : Module.finrank Real (Submodule.span Real (Set.range f)) = 2 := by simpa using (finrank_span_eq_card (R := Real) (M := Fin 2 → Real) (b := f) hlin) have hspan_top : Submodule.span Real (Set.range f) = ⊤ := by apply Submodule.eq_top_of_finrank_eq have hV : Module.finrank Real (Fin 2 → Real) = 2 := by simp simpa [hV] using hspan_finrank have hsp : (⊤ : Submodule Real (Fin 2 → Real)) ≤ Submodule.span Real (Set.range f) := by simp [hspan_top] let b : Module.Basis (Fin 2) Real (Fin 2 → Real) := Module.Basis.mk hlin hsp have hv : v = b 0 := by simp [b, f] have hw : w = b 1 := by simp [b, f] let A : (Fin 2 → Real) ≃ₗ[Real] (Fin 2 → Real) := b.equivFun have Av : A v = ![(1 : Real), 0] := by ext i fin_cases i <;> simp [A, hv, Module.Basis.equivFun_self] have Aw : A w = ![(0 : Real), 1] := by ext i fin_cases i <;> simp [A, hw, Module.Basis.equivFun_self] let e : (Fin 2 → Real) ≃ᵃ[Real] (Fin 2 → Real) := AffineEquiv.ofLinearEquiv A x0 0 have hdir_eq : (Real ∙ v) = L.direction := by apply Submodule.eq_of_le_of_finrank_eq · intro x hx rcases (Submodule.mem_span_singleton).1 hx with ⟨a, rfl⟩ exact L.direction.smul_mem a hvdir · have hvdim : Module.finrank Real (Real ∙ v) = 1 := by simpa using (finrank_span_singleton (K := Real) (v := v) hv0) simpa [hL] using hvdim have hLimage : e '' (L : Set (Fin 2 → Real)) = cor1717_xAxis := by ext x constructor · rintro ⟨y, hy, rfl⟩ have hy_dir : y -ᵥ x0 ∈ L.direction := AffineSubspace.vsub_mem_direction hy hx0L have hy_dir' : y -ᵥ x0 ∈ (Real ∙ v) := by simpa [hdir_eq] using hy_dir rcases (Submodule.mem_span_singleton).1 hy_dir' with ⟨a, ha⟩ have hx' : e y = a • ![(1 : Real), 0] := by calc e y = A (y -ᵥ x0) +ᵥ (0 : Fin 2 → Real) := by simp [e, AffineEquiv.ofLinearEquiv_apply] _ = A (a • v) +ᵥ (0 : Fin 2 → Real) := by simp [ha] _ = a • ![(1 : Real), 0] := by simp [A, Av, vadd_eq_add] simp [cor1717_xAxis, hx'] · intro hx have hx1 : x 1 = 0 := by simpa [cor1717_xAxis] using hx let a : Real := x 0 have hx_eq : x = a • ![(1 : Real), 0] := by ext i fin_cases i · simp [a] · simp [a, hx1] have hmem : a • v ∈ L.direction := by exact L.direction.smul_mem a hvdir have hxL : a • v +ᵥ x0 ∈ (L : Set (Fin 2 → Real)) := AffineSubspace.vadd_mem_of_mem_direction hmem hx0L refine ⟨a • v +ᵥ x0, hxL, ?_⟩ calc e (a • v +ᵥ x0) = A (a • v) +ᵥ (0 : Fin 2 → Real) := by simp [e, AffineEquiv.ofLinearEquiv_apply] _ = a • ![(1 : Real), 0] := by simp [A, Av, vadd_eq_add] _ = x := by simp [hx_eq] have hpimage : e p = cor1717_p := by calc e p = A w +ᵥ (0 : Fin 2 → Real) := by simp [e, AffineEquiv.ofLinearEquiv_apply, w] _ = cor1717_p := by simp [Aw, cor1717_p, vadd_eq_add] exact ⟨e, hLimage, hpimage⟩

Crollary 17.1.7 (Convex hull of a closed set need not be closed), particular case: if Unknown identifier `S`S is the union of an affine line in and a point not on that line, then is not closed.

theorem not_isClosed_conv_line_union_singleton {L : AffineSubspace Real (Fin 2 → Real)} {p : Fin 2 → Real} (hL : Module.finrank Real L.direction = 1) (hp : p ∉ (L : Set (Fin 2 → Real))) : ¬ IsClosed (conv ((L : Set (Fin 2 → Real)) ∪ {p})) := by intro hclosed rcases exists_affineEquiv_image_line_eq_xAxis_and_map_point hL hp with ⟨e, hLimage, hpimage⟩ have hclosed_image : IsClosed (e '' conv ((L : Set (Fin 2 → Real)) ∪ {p})) := by exact (e.toHomeomorphOfFiniteDimensional.isClosed_image).2 hclosed have himage_sets : e '' ((L : Set (Fin 2 → Real)) ∪ {p}) = cor1717_xAxis ∪ {cor1717_p} := by ext x constructor · rintro ⟨y, hy, rfl⟩ rcases hy with hyL | hyp · have hx : e y ∈ cor1717_xAxis := by have : e y ∈ e '' (L : Set (Fin 2 → Real)) := ⟨y, hyL, rfl⟩ simpa [hLimage] using this exact Or.inl hx · have hy_eq : y = p := by simpa using hyp have : e y = cor1717_p := by simpa [hy_eq] using hpimage exact Or.inr (by simp [this]) · intro hx rcases hx with hx | hx · have hx' : x ∈ e '' (L : Set (Fin 2 → Real)) := by simpa [hLimage] using hx rcases hx' with ⟨y, hyL, rfl⟩ exact ⟨y, Or.inl hyL, rfl⟩ · have hx' : x = cor1717_p := by simpa using hx refine ⟨p, Or.inr (by simp), ?_⟩ simp [hx', hpimage] have himage_sets' : e '' insert p (L : Set (Fin 2 → Real)) = insert cor1717_p cor1717_xAxis := by simpa [Set.union_singleton] using himage_sets have himage_insert : e '' conv (insert p (L : Set (Fin 2 → Real))) = conv (insert cor1717_p cor1717_xAxis) := by calc e '' conv (insert p (L : Set (Fin 2 → Real))) = conv (e '' insert p (L : Set (Fin 2 → Real))) := by simpa [conv] using (AffineMap.image_convexHull (f := (e : (Fin 2 → Real) →ᵃ[Real] (Fin 2 → Real))) (insert p (L : Set (Fin 2 → Real)))) _ = conv (insert cor1717_p cor1717_xAxis) := by simp [himage_sets'] have himage : e '' conv ((L : Set (Fin 2 → Real)) ∪ {p}) = conv (cor1717_xAxis ∪ {cor1717_p}) := by simpa [Set.union_singleton] using himage_insert have hclosed' : IsClosed (conv (cor1717_xAxis ∪ {cor1717_p})) := by have hclosed_image' : IsClosed (e '' conv (insert p (L : Set (Fin 2 → Real)))) := by simpa [Set.union_singleton] using hclosed_image have hclosed'' : IsClosed (conv (insert cor1717_p cor1717_xAxis)) := by simpa [himage_insert] using hclosed_image' simpa [Set.union_singleton] using hclosed'' exact cor1717_not_isClosed_conv_xAxis_union_point hclosed'

Convex weights are exactly points in the standard simplex.

lemma isConvexWeights_iff_mem_stdSimplex {m : Nat} {w : Fin m → Real} : IsConvexWeights m w ↔ w ∈ stdSimplex Real (Fin m) := by simp [IsConvexWeights, stdSimplex]

The set of convex combinations of Unknown identifier `m`m points from closure sorry : Set ?m.1closure Unknown identifier `S`S.

def convexCombinationSet {n : Nat} (S : Set (Fin n → Real)) (m : Nat) : Set (Fin n → Real) := {y : Fin n → Real | ∃ (x : Fin m → closure S) (w : Fin m → Real), IsConvexWeights m w ∧ y = convexCombination n m (fun i => (x i : Fin n → Real)) w}

The Unknown identifier `m`m-point convex-combination set is compact when closure sorry : Set ?m.1closure Unknown identifier `S`S is compact.

lemma isCompact_convexCombinationSet_of_isCompact {n m : Nat} {S : Set (Fin n → Real)} (hS : IsCompact (closure S)) : IsCompact (convexCombinationSet (n := n) (S := S) m) := by classical haveI : CompactSpace (closure S) := (isCompact_iff_compactSpace.mp hS) let f : (stdSimplex Real (Fin m) × (Fin m → closure S)) → Fin n → Real := fun p => convexCombination n m (fun i => (p.2 i : Fin n → Real)) p.1 have hf : Continuous f := by classical have hf' : Continuous fun p : (stdSimplex Real (Fin m) × (Fin m → closure S)) => ∑ i, (p.1 i) • (p.2 i : Fin n → Real) := by refine (continuous_finset_sum (s := Finset.univ) (f := fun i (p : stdSimplex Real (Fin m) × (Fin m → closure S)) => (p.1 i) • (p.2 i : Fin n → Real))) ?_ intro i hi have h1 : Continuous fun p : (stdSimplex Real (Fin m) × (Fin m → closure S)) => (p.1 : Fin m → Real) i := by have h1' : Continuous fun p : (stdSimplex Real (Fin m) × (Fin m → closure S)) => (p.1 : Fin m → Real) := continuous_subtype_val.comp continuous_fst simpa using (continuous_apply i).comp h1' have h2 : Continuous fun p : (stdSimplex Real (Fin m) × (Fin m → closure S)) => (p.2 i : Fin n → Real) := by have h2' : Continuous fun p : (stdSimplex Real (Fin m) × (Fin m → closure S)) => (p.2 i) := (continuous_apply i).comp continuous_snd exact continuous_subtype_val.comp h2' exact h1.smul h2 simpa [f, convexCombination] using hf' have himage : convexCombinationSet (n := n) (S := S) m = f '' (Set.univ : Set (stdSimplex Real (Fin m) × (Fin m → closure S))) := by ext y constructor · rintro ⟨x, w, hw, rfl⟩ have hw' : w ∈ stdSimplex Real (Fin m) := (isConvexWeights_iff_mem_stdSimplex).1 hw refine ⟨(⟨w, hw'⟩, x), by simp, rfl⟩ · rintro ⟨p, -, rfl⟩ have hw : IsConvexWeights m (p.1 : Fin m → Real) := (isConvexWeights_iff_mem_stdSimplex).2 p.1.property exact ⟨p.2, (p.1 : Fin m → Real), hw, rfl⟩ have hcompact : IsCompact (f '' (Set.univ : Set (stdSimplex Real (Fin m) × (Fin m → closure S)))) := (isCompact_univ.image hf) simpa [himage] using hcompact

Carathéodory-style union: conv (closure sorry) : Set (Fin ?m.1 → ℝ)conv (closure Unknown identifier `S`S) is the union of Unknown identifier `m`m-point combination sets.

lemma conv_closure_eq_iUnion_convexCombinationSet {n : Nat} (S : Set (Fin n → Real)) : conv (closure S) = ⋃ m : Fin (n + 2), convexCombinationSet (n := n) (S := S) m := by classical ext y constructor · intro hy rcases caratheodory (n := n) (S := closure S) (x := y) hy with ⟨m, hm_le, x, w, hxS, hw, hy_eq⟩ have hm_lt : m < n + 2 := Nat.lt_succ_of_le hm_le let x' : Fin m → closure S := fun i => ⟨x i, hxS i⟩ have hy_mem : y ∈ convexCombinationSet (n := n) (S := S) m := by refine ⟨x', w, hw, ?_⟩ simpa [x'] using hy_eq refine Set.mem_iUnion.2 ?_ exact ⟨⟨m, hm_lt⟩, by simpa using hy_mem⟩ · intro hy rcases Set.mem_iUnion.1 hy with ⟨m, hm⟩ rcases hm with ⟨x, w, hw, rfl⟩ have hcomb : IsConvexCombination n m (fun i => (x i : Fin n → Real)) (convexCombination n m (fun i => (x i : Fin n → Real)) w) := isConvexCombination_of_isConvexWeights n m (fun i => (x i : Fin n → Real)) w hw have hxS : ∀ i, (x i : Fin n → Real) ∈ closure S := fun i => (x i).property have hmem : convexCombination n m (fun i => (x i : Fin n → Real)) w ∈ convexHull Real (closure S) := by refine (mem_convexHull_iff_exists_fin_isConvexCombination n (closure S) _).2 ?_ exact ⟨m, (fun i => (x i : Fin n → Real)), hxS, hcomb⟩ simpa [conv] using hmem

The easy inclusion conv (closure sorry) ⊆ closure (conv sorry) : Propconv (closure Unknown identifier `S`S) ⊆ closure (conv Unknown identifier `S`S).

lemma thm172_conv_closure_subset_closure_conv {n : Nat} {S : Set (Fin n → Real)} : conv (closure S) ⊆ closure (conv S) := by have hsub : closure S ⊆ closure (conv S) := closure_mono (by simpa [conv] using (subset_convexHull Real S)) have hconv : Convex Real (closure (conv S)) := by have hconv' : Convex Real (conv S) := by simpa [conv] using (convex_convexHull Real S) exact hconv'.closure simpa [conv] using (convexHull_min hsub hconv)

Boundedness yields closedness of conv (closure sorry) : Set (Fin ?m.1 → ℝ)conv (closure Unknown identifier `S`S).

lemma thm172_isClosed_conv_closure_of_isBounded {n : Nat} {S : Set (Fin n → Real)} (hS : Bornology.IsBounded S) : IsClosed (conv (closure S)) := by classical have hcompactS : IsCompact (closure S) := hS.isCompact_closure have hcompact_comb : ∀ m : Fin (n + 2), IsCompact (convexCombinationSet (n := n) (S := S) m) := by intro m exact isCompact_convexCombinationSet_of_isCompact (n := n) (S := S) (m := m) hcompactS have hconv_eq : conv (closure S) = ⋃ m : Fin (n + 2), convexCombinationSet (n := n) (S := S) m := conv_closure_eq_iUnion_convexCombinationSet (n := n) (S := S) have hcompact : IsCompact (conv (closure S)) := by have : IsCompact (⋃ m : Fin (n + 2), convexCombinationSet (n := n) (S := S) m) := isCompact_iUnion hcompact_comb simpa [hconv_eq] using this exact hcompact.isClosed

The bounded inclusion closure (conv sorry) ⊆ conv (closure sorry) : Propclosure (conv Unknown identifier `S`S) ⊆ conv (closure Unknown identifier `S`S).

lemma thm172_closure_conv_subset_conv_closure_of_isBounded {n : Nat} {S : Set (Fin n → Real)} (hS : Bornology.IsBounded S) : closure (conv S) ⊆ conv (closure S) := by have hconv_mono : conv S ⊆ conv (closure S) := by simpa [conv] using (convexHull_mono (subset_closure (s := S))) exact closure_minimal hconv_mono (thm172_isClosed_conv_closure_of_isBounded (n := n) (S := S) hS)

Theorem 17.2. If Unknown identifier `S`S is a bounded set of points in , then closure (conv sorry) = conv (closure sorry) : Propclosure (conv Unknown identifier `S`S) = conv (closure Unknown identifier `S`S). In particular, if Unknown identifier `S`S is closed and bounded, then conv sorry : Set (Fin ?m.1 → ℝ)conv Unknown identifier `S`S is closed and bounded.

theorem closure_conv_eq_conv_closure_of_isBounded {n : Nat} {S : Set (Fin n → Real)} (hS : Bornology.IsBounded S) : closure (conv S) = conv (closure S) := by refine Set.Subset.antisymm ?_ ?_ · exact thm172_closure_conv_subset_conv_closure_of_isBounded (n := n) (S := S) hS · exact thm172_conv_closure_subset_closure_conv (n := n) (S := S)

Theorem 17.2 (in particular). If Unknown identifier `S`S is closed and bounded, then conv sorry : Set (Fin ?m.1 → ℝ)conv Unknown identifier `S`S is closed and bounded.

theorem isClosed_and_isBounded_conv_of_isClosed_and_isBounded {n : Nat} {S : Set (Fin n → Real)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) : IsClosed (conv S) ∧ Bornology.IsBounded (conv S) := by have hclosed : IsClosed (conv S) := by have hclosed' : IsClosed (conv (closure S)) := thm172_isClosed_conv_closure_of_isBounded (n := n) (S := S) hS_bdd simpa [hS_closed.closure_eq] using hclosed' have hbdd : Bornology.IsBounded (conv S) := by simpa [conv] using (isBounded_convexHull (s := S)).2 hS_bdd exact ⟨hclosed, hbdd⟩

Compactness of a closed bounded subset of .

lemma cor1721_isCompact_S {n : Nat} {S : Set (Fin n → Real)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) : IsCompact S := by have hcomp : IsCompact (closure S) := hS_bdd.isCompact_closure simpa [hS_closed.closure_eq] using hcomp

A continuous function on a nonempty compact set is bounded below.

lemma cor1721_exists_lowerBound_on_S {n : Nat} {S : Set (Fin n → Real)} (hS_compact : IsCompact S) (hS_ne : S.Nonempty) {f : (Fin n → Real) → Real} (hf : ContinuousOn f S) : ∃ m : Real, ∀ x ∈ S, m ≤ f x := by rcases hS_compact.exists_isMinOn hS_ne hf with ⟨x0, hx0S, hx0min⟩ have hx0min' : ∀ x ∈ S, f x0 ≤ f x := by simpa [IsMinOn, Filter.eventually_principal] using hx0min refine ⟨f x0, ?_⟩ intro x hx exact hx0min' x hx

Properness of convexHullFunction {n : ℕ} (g : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → ERealconvexHullFunction from a global lower bound on Unknown identifier `f`f over Unknown identifier `S`S.

lemma cor1721_properConvexFunctionOn_convexHullFunction_fExt {n : Nat} {S : Set (Fin n → Real)} (hS_ne : S.Nonempty) {f : (Fin n → Real) → Real} {m : Real} (hm : ∀ x ∈ S, m ≤ f x) : (let fExt : (Fin n → Real) → EReal := fun x => (f x : EReal) + indicatorFunction S x ProperConvexFunctionOn (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt)) := by classical intro fExt have hconv : ConvexFunctionOn (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt) := by simpa using (convexHullFunction_greatest_convex_minorant (g := fExt)).1 have hle : convexHullFunction fExt ≤ fExt := (convexHullFunction_greatest_convex_minorant (g := fExt)).2.1 rcases hS_ne with ⟨x0, hx0S⟩ have hmem : (x0, f x0) ∈ epigraph (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt) := by refine (mem_epigraph_univ_iff (f := convexHullFunction fExt)).2 ?_ have hle' := hle x0 simpa [fExt, indicatorFunction, hx0S] using hle' have hne_epi : Set.Nonempty (epigraph (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt)) := ⟨(x0, f x0), hmem⟩ have hconst_conv : ConvexFunctionOn (Set.univ : Set (Fin n → Real)) (fun _ => (m : EReal)) := (properConvexFunctionOn_const (n := n) m).1 have hconst_le : (fun _ => (m : EReal)) ≤ fExt := by intro x by_cases hx : x ∈ S · have hmx : (m : EReal) ≤ (f x : EReal) := (EReal.coe_le_coe_iff).2 (hm x hx) simpa [fExt, indicatorFunction, hx] using hmx · simp [fExt, indicatorFunction, hx] have hconst_le_fconv : (fun _ => (m : EReal)) ≤ convexHullFunction fExt := (convexHullFunction_greatest_convex_minorant (g := fExt)).2.2 (fun _ => (m : EReal)) hconst_conv hconst_le have hnotbot : ∀ x ∈ (Set.univ : Set (Fin n → Real)), convexHullFunction fExt x ≠ (⊥ : EReal) := by intro x _ hxbot have hle' := hconst_le_fconv x have hEq : (m : EReal) = (⊥ : EReal) := by have hle'' := hle' simp [hxbot] at hle'' exact (EReal.coe_ne_bot m) hEq exact ⟨hconv, hne_epi, by simpa using hnotbot⟩

The extension Unknown identifier `fExt`fExt never takes the value ⊥ : ?m.1⊥.

lemma cor1721_fExt_ne_bot {n : Nat} {S : Set (Fin n → Real)} {f : (Fin n → Real) → Real} : (let fExt : (Fin n → Real) → EReal := fun x => (f x : EReal) + indicatorFunction S x ∀ x, fExt x ≠ (⊥ : EReal)) := by intro fExt x by_cases hx : x ∈ S <;> simp [fExt, indicatorFunction, hx]

The graph of Unknown identifier `f`f over a compact set is compact.

lemma cor1721_isCompact_graph {n : Nat} {S : Set (Fin n → Real)} (hS : IsCompact S) {f : (Fin n → Real) → Real} (hf : ContinuousOn f S) : IsCompact ((fun x => (x, f x)) '' S) := by have hcont : ContinuousOn (fun x : Fin n → Real => (x, f x)) S := by simpa using (continuousOn_id.prodMk hf) exact hS.image_of_continuousOn hcont

The convex hull of the graph is compact in ℝ ^ {sorry + 1} : Typeℝ^{Unknown identifier `n`n+1}.

lemma cor1721_isCompact_convexHull_graph {n : Nat} {S : Set (Fin n → Real)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → Real) → Real} (hf : ContinuousOn f S) : (let F : Set ((Fin n → Real) × Real) := (fun x => (x, f x)) '' S IsCompact (convexHull ℝ F)) := by classical intro F have hS_compact : IsCompact S := cor1721_isCompact_S (S := S) hS_closed hS_bdd have hF_compact : IsCompact F := cor1721_isCompact_graph (S := S) hS_compact (f := f) hf let e : ((Fin n → Real) × Real) ≃L[Real] (Fin (n + 1) → Real) := (prodLinearEquiv_append_coord (n := n)).toContinuousLinearEquiv let T : Set (Fin (n + 1) → Real) := e '' F have hT_compact : IsCompact T := hF_compact.image e.continuous have hT_bdd : Bornology.IsBounded T := hT_compact.isBounded have hT_closed : IsClosed T := hT_compact.isClosed have hconv_closed : IsClosed (conv (closure T)) := thm172_isClosed_conv_closure_of_isBounded (n := n + 1) (S := T) hT_bdd have hconv_closed' : IsClosed (conv T) := by simpa [hT_closed.closure_eq] using hconv_closed have hconv_bdd : Bornology.IsBounded (conv T) := by simpa [conv] using (isBounded_convexHull (s := T)).2 hT_bdd have hconv_compact : IsCompact (conv T) := (Metric.isCompact_iff_isClosed_bounded).2 ⟨hconv_closed', hconv_bdd⟩ have hpre : (e.symm : _ → _) '' T = F := by ext p constructor · rintro ⟨y, ⟨x, hx, rfl⟩, rfl⟩ simpa using hx · intro hp refine ⟨e p, ?_, by simp⟩ exact ⟨p, hp, rfl⟩ have himage : (e.symm : _ → _) '' (conv T) = convexHull ℝ F := by have h := (LinearMap.image_convexHull (f := e.symm.toLinearMap) (s := T)) simpa [conv, hpre] using h have hcomp_image : IsCompact ((e.symm : _ → _) '' conv T) := hconv_compact.image e.symm.continuous simpa [himage] using hcomp_image

The Minkowski sum of the vertical ray and the convex hull of the graph is closed.

lemma cor1721_isClosed_K_add_convexHull_graph {n : Nat} {S : Set (Fin n → Real)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → Real) → Real} (hf : ContinuousOn f S) : (let F : Set ((Fin n → Real) × Real) := (fun x => (x, f x)) '' S let K : Set ((Fin n → Real) × Real) := {p | p.1 = 0 ∧ 0 ≤ p.2} IsClosed (K + convexHull ℝ F)) := by classical intro F K have hK_closed : IsClosed K := by have hK1 : IsClosed {p : (Fin n → Real) × Real | p.1 = 0} := isClosed_eq continuous_fst continuous_const have hK2 : IsClosed {p : (Fin n → Real) × Real | 0 ≤ p.2} := isClosed_le continuous_const continuous_snd have hK : K = {p : (Fin n → Real) × Real | p.1 = 0} ∩ {p : (Fin n → Real) × Real | 0 ≤ p.2} := by ext p constructor · intro hp exact ⟨hp.1, hp.2⟩ · intro hp exact ⟨hp.1, hp.2⟩ simpa [hK] using hK1.inter hK2 have hF_compact : IsCompact (convexHull ℝ F) := by simpa using (cor1721_isCompact_convexHull_graph (S := S) hS_closed hS_bdd (f := f) hf) exact IsClosed.add_right_of_isCompact hK_closed hF_compact

The epigraph of the convex hull function is .

lemma cor1721_epigraph_eq_K_add_convexHull_graph {n : Nat} {S : Set (Fin n → Real)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → Real) → Real} (hf : ContinuousOn f S) : (let fExt : (Fin n → Real) → EReal := fun x => (f x : EReal) + indicatorFunction S x let F : Set ((Fin n → Real) × Real) := (fun x => (x, f x)) '' S let K : Set ((Fin n → Real) × Real) := {p | p.1 = 0 ∧ 0 ≤ p.2} epigraph (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt) = K + convexHull ℝ F) := by classical intro fExt F K let C : Set ((Fin n → Real) × Real) := K + convexHull ℝ F have hEpi_fExt : epigraph (Set.univ : Set (Fin n → Real)) fExt = K + F := by ext p rcases p with ⟨x, μ⟩ constructor · intro hp have hle : fExt x ≤ (μ : EReal) := (mem_epigraph_univ_iff (f := fExt)).1 hp have hx : x ∈ S := by by_contra hx have htop : (⊤ : EReal) ≤ (μ : EReal) := by have hle_top := hle simp [fExt, indicatorFunction, hx] at hle_top have hEq : (μ : EReal) = ⊤ := (top_le_iff).1 htop exact (EReal.coe_ne_top _ hEq).elim have hle' : (f x : EReal) ≤ (μ : EReal) := by simpa [fExt, indicatorFunction, hx] using hle have hle'' : f x ≤ μ := (EReal.coe_le_coe_iff).1 hle' have hk : (0, μ - f x) ∈ K := by refine ⟨by simp, ?_⟩ linarith have hq : (x, f x) ∈ F := ⟨x, hx, rfl⟩ have hsum : (0, μ - f x) + (x, f x) = (x, μ) := by ext <;> simp [sub_eq_add_neg, add_comm, add_left_comm] exact (Set.mem_add).2 ⟨(0, μ - f x), hk, (x, f x), hq, hsum⟩ · intro hp rcases (Set.mem_add).1 hp with ⟨k, hk, q, hq, hsum⟩ rcases hq with ⟨x', hx', rfl⟩ have hsum0 := congrArg Prod.fst hsum have hx_eq : x' = x := by simpa [hk.1, add_comm, add_left_comm, add_assoc] using hsum0 have hx : x ∈ S := by simpa [hx_eq] using hx' have hle' : (f x : EReal) ≤ ((f x + k.2 : Real) : EReal) := by have hle'' : f x ≤ f x + k.2 := by exact le_add_of_nonneg_right hk.2 exact (EReal.coe_le_coe_iff).2 hle'' have hmem : fExt x ≤ ((f x + k.2 : Real) : EReal) := by simpa [fExt, indicatorFunction, hx] using hle' have hle : fExt x ≤ (μ : EReal) := by have hsum1 := congrArg Prod.snd hsum have hsum3 : k.2 + f x = μ := by simpa [hx_eq] using hsum1 simpa [hsum3, add_comm, add_left_comm, add_assoc] using hmem exact (mem_epigraph_univ_iff (f := fExt)).2 hle have hK_conv : Convex Real K := by intro p hp q hq a b ha hb hsum rcases hp with ⟨hp1, hp2⟩ rcases hq with ⟨hq1, hq2⟩ refine ⟨?_, ?_⟩ · have : (a • p + b • q).1 = 0 := by simp [hp1, hq1] simpa using this · have hp2' : 0 ≤ a * p.2 := mul_nonneg ha hp2 have hq2' : 0 ≤ b * q.2 := mul_nonneg hb hq2 have : 0 ≤ a * p.2 + b * q.2 := add_nonneg hp2' hq2' simpa [smul_eq_mul, add_comm, add_left_comm, add_assoc] using this have hconvHull_epi : convexHull ℝ (epigraph (Set.univ : Set (Fin n → Real)) fExt) = C := by have hconv_add : convexHull ℝ (K + F) = convexHull ℝ K + convexHull ℝ F := by simpa using (convexHull_add (R := Real) (s := K) (t := F)) simpa [hEpi_fExt, C, hK_conv.convexHull_eq] using hconv_add have hconvFun_eq : convexHullFunction fExt = fun x => sInf ((fun μ : ℝ => (μ : EReal)) '' { μ : ℝ | (x, μ) ∈ C }) := by funext x simp [convexHullFunction_eq_inf_section, hconvHull_epi, C] ext p rcases p with ⟨x, μ⟩ constructor · intro hp have hle : convexHullFunction fExt x ≤ (μ : EReal) := (mem_epigraph_univ_iff (f := convexHullFunction fExt)).1 hp have hle' : sInf ((fun μ : ℝ => (μ : EReal)) '' { μ : ℝ | (x, μ) ∈ C }) ≤ (μ : EReal) := by simpa [hconvFun_eq] using hle let Fx : Set ((Fin n → Real) × Real) := convexHull ℝ F ∩ {q | q.1 = x} have hFx_nonempty : Fx.Nonempty := by by_contra hFx have hSx_empty : { μ : ℝ | (x, μ) ∈ C } = ∅ := by ext μ' constructor · intro hμ' rcases (Set.mem_add).1 hμ' with ⟨k, hk, q, hq, hsum⟩ have hq1 : q.1 = x := by have hsum0 := congrArg Prod.fst hsum simpa [hk.1] using hsum0 have hFx' : q ∈ Fx := ⟨hq, hq1⟩ exact (hFx ⟨q, hFx'⟩).elim · intro hμ' cases hμ' have htop : (⊤ : EReal) ≤ (μ : EReal) := by have hle_top := hle' simp [hSx_empty] at hle_top have hEq : (μ : EReal) = ⊤ := (top_le_iff).1 htop exact (EReal.coe_ne_top _ hEq).elim have hFx_compact : IsCompact Fx := by have hF_compact : IsCompact (convexHull ℝ F) := by simpa using (cor1721_isCompact_convexHull_graph (S := S) hS_closed hS_bdd (f := f) hf) have hclosed : IsClosed {q : (Fin n → Real) × Real | q.1 = x} := isClosed_eq continuous_fst continuous_const simpa [Fx] using hF_compact.inter_right hclosed have hcont_snd : ContinuousOn (fun q : (Fin n → Real) × Real => q.2) Fx := by simpa using (continuous_snd.continuousOn : ContinuousOn (fun q => q.2) Fx) rcases hFx_compact.exists_isMinOn hFx_nonempty hcont_snd with ⟨q0, hq0Fx, hq0min⟩ rcases hq0Fx with ⟨hq0F, hq0x⟩ have hq0x' : q0.1 = x := by simpa using hq0x have hq0eq : q0 = (x, q0.2) := by ext <;> simp [hq0x'] have hq0C : (x, q0.2) ∈ C := by have hK0 : (0, (0 : Real)) ∈ K := by simp [K] have hmem := Set.add_mem_add (s := K) (t := convexHull ℝ F) hK0 hq0F have hmem' : (0, (0 : Real)) + q0 ∈ C := by simpa [C] using hmem have hsum : (0, (0 : Real)) + q0 = (x, q0.2) := by rw [hq0eq] ext <;> simp exact hsum ▸ hmem' have hq0min' : ∀ q ∈ Fx, q0.2 ≤ q.2 := by have hq0min' : ∀ᶠ q in Filter.principal Fx, q0.2 ≤ q.2 := by simpa [IsMinOn, IsMinFilter] using hq0min simpa [Filter.eventually_principal] using hq0min' have hq0lb : ∀ μ' ∈ { μ : ℝ | (x, μ) ∈ C }, q0.2 ≤ μ' := by intro μ' hμ' rcases (Set.mem_add).1 hμ' with ⟨k, hk, q, hq, hsum⟩ have hq1 : q.1 = x := by have hsum0 := congrArg Prod.fst hsum simpa [hk.1] using hsum0 have hqFx : q ∈ Fx := ⟨hq, hq1⟩ have hq0le : q0.2 ≤ q.2 := hq0min' q hqFx have hqle : q.2 ≤ μ' := by have hsum1 := congrArg Prod.snd hsum have hsum2 : q.2 + k.2 = μ' := by simpa [add_comm, add_left_comm, add_assoc] using hsum1 linarith [hk.2, hsum2] exact le_trans hq0le hqle have hSx_eq : sInf ((fun μ : ℝ => (μ : EReal)) '' { μ : ℝ | (x, μ) ∈ C }) = (q0.2 : EReal) := by have hle_sInf : sInf ((fun μ : ℝ => (μ : EReal)) '' { μ : ℝ | (x, μ) ∈ C }) ≤ (q0.2 : EReal) := sInf_le ⟨q0.2, hq0C, rfl⟩ have hge_sInf : (q0.2 : EReal) ≤ sInf ((fun μ : ℝ => (μ : EReal)) '' { μ : ℝ | (x, μ) ∈ C }) := by refine le_sInf ?_ intro z hz rcases hz with ⟨μ', hμ', rfl⟩ exact (EReal.coe_le_coe_iff).2 (hq0lb μ' hμ') exact le_antisymm hle_sInf hge_sInf have hq0leμ : q0.2 ≤ μ := by have hle'' : (q0.2 : EReal) ≤ (μ : EReal) := by simpa [hSx_eq] using hle' exact (EReal.coe_le_coe_iff).1 hle'' have hk : (0, μ - q0.2) ∈ K := by refine ⟨by simp, ?_⟩ linarith have hsum : (0, μ - q0.2) + q0 = (x, μ) := by ext <;> simp [hq0x', sub_eq_add_neg, add_comm, add_left_comm] exact (Set.mem_add).2 ⟨(0, μ - q0.2), hk, q0, hq0F, hsum⟩ · intro hp have hle' : sInf ((fun μ : ℝ => (μ : EReal)) '' { μ : ℝ | (x, μ) ∈ C }) ≤ (μ : EReal) := sInf_le ⟨μ, hp, rfl⟩ have hle : convexHullFunction fExt x ≤ (μ : EReal) := by simpa [hconvFun_eq] using hle' exact (mem_epigraph_univ_iff (f := convexHullFunction fExt)).2 hle

Closedness of the epigraph of the convex hull function for Unknown identifier `fExt`fExt.

lemma cor1721_isClosed_epigraph_convexHullFunction_fExt {n : Nat} {S : Set (Fin n → Real)} (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → Real) → Real} (hf : ContinuousOn f S) : (let fExt : (Fin n → Real) → EReal := fun x => (f x : EReal) + indicatorFunction S x IsClosed (epigraph (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt))) := by classical intro fExt let F : Set ((Fin n → Real) × Real) := (fun x => (x, f x)) '' S let K : Set ((Fin n → Real) × Real) := {p | p.1 = 0 ∧ 0 ≤ p.2} have hclosed : IsClosed (K + convexHull ℝ F) := by simpa [F, K] using (cor1721_isClosed_K_add_convexHull_graph (S := S) hS_closed hS_bdd (f := f) hf) have hEq : epigraph (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt) = K + convexHull ℝ F := by simpa [fExt, F, K] using (cor1721_epigraph_eq_K_add_convexHull_graph (S := S) hS_closed hS_bdd (f := f) hf) simpa [hEq] using hclosed

Corollary 17.2.1. Let Unknown identifier `S`S be a nonempty closed bounded set in . Let Unknown identifier `f`f be a continuous real-valued function on Unknown identifier `S`S, and extend it by for Unknown identifier `x`sorry ∉ sorry : Propx ∉ Unknown identifier `S`S. Then conv sorry : Set (Fin ?m.1 → ℝ)conv Unknown identifier `f`f (here: convexHullFunction {n : ℕ} (g : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → ERealconvexHullFunction applied to the extension) is a closed proper convex function.

theorem closedConvex_and_properConvexFunctionOn_convexHullFunction_of_continuousOn_closed_bounded {n : Nat} {S : Set (Fin n → Real)} (hS_ne : S.Nonempty) (hS_closed : IsClosed S) (hS_bdd : Bornology.IsBounded S) {f : (Fin n → Real) → Real} (hf : ContinuousOn f S) : (let fExt : (Fin n → Real) → EReal := fun x => (f x : EReal) + indicatorFunction S x ClosedConvexFunction (n := n) (convexHullFunction fExt) ∧ ProperConvexFunctionOn (S := (Set.univ : Set (Fin n → Real))) (convexHullFunction fExt)) := by classical let fExt : (Fin n → Real) → EReal := fun x => (f x : EReal) + indicatorFunction S x have hS_compact : IsCompact S := cor1721_isCompact_S (S := S) hS_closed hS_bdd rcases cor1721_exists_lowerBound_on_S (S := S) hS_compact hS_ne hf with ⟨m, hm⟩ have hproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt) := by simpa [fExt] using (cor1721_properConvexFunctionOn_convexHullFunction_fExt (S := S) hS_ne (f := f) hm) have hclosed_epi : IsClosed (epigraph (Set.univ : Set (Fin n → Real)) (convexHullFunction fExt)) := by simpa [fExt] using (cor1721_isClosed_epigraph_convexHullFunction_fExt (S := S) hS_closed hS_bdd (f := f) hf) have hclosed_sub : ∀ α : Real, IsClosed {x | convexHullFunction fExt x ≤ (α : EReal)} := (lowerSemicontinuous_iff_closed_sublevel_iff_closed_epigraph (f := convexHullFunction fExt)).2.mpr hclosed_epi have hls : LowerSemicontinuous (convexHullFunction fExt) := (lowerSemicontinuous_iff_closed_sublevel_iff_closed_epigraph (f := convexHullFunction fExt)).1.mpr hclosed_sub have hclosed : ClosedConvexFunction (convexHullFunction fExt) := (properConvexFunction_closed_iff_lowerSemicontinuous (f := convexHullFunction fExt) hproper).2 hls exact ⟨hclosed, hproper⟩

Definition 17.2.2 (A convex function defined as a supremum), LaTeX label .

Let and let (modeled here as ). Define by

.

In Fin sorry → ℝ : TypeFin Unknown identifier `n`n → ℝ, the inner product is expressed as ∑ i, sorry * sorry : ?m.2∑ i, Unknown identifier `z`z i * Unknown identifier `x`x i.

noncomputable def supremumInnerSub {n : Nat} (S : Set (Fin n → Real)) (f : S → EReal) (z : Fin n → Real) : EReal := sSup (Set.range fun x : S => ((∑ i, z i * (x.1 i) : Real) : EReal) - f x)
end Section17end Chap04