Convex Analysis (Rockafellar, 1970) -- Chapter 03 -- Section 16 -- Part 14

Closure of a sublevel set matches the sublevel of the convex-function closure when the domain is Fin sorry → ℝ : TypeFin Unknown identifier `n`n → ℝ.

lemma section16_closure_sublevel_eq_sublevel_convexFunctionClosure_one_fin {n : Nat} {h : (Fin n → ℝ) → EReal} (hh : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) h) (hInf : iInf (fun x => h x) < (1 : EReal)) : closure {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} = {xStar : Fin n → ℝ | convexFunctionClosure h xStar ≤ (1 : EReal)} := by classical let e := EuclideanSpace.equiv (Fin n) ℝ let A : Set (EuclideanSpace ℝ (Fin n)) := {x : EuclideanSpace ℝ (Fin n) | h (x : Fin n → ℝ) ≤ (1 : EReal)} let B : Set (EuclideanSpace ℝ (Fin n)) := {x : EuclideanSpace ℝ (Fin n) | convexFunctionClosure h (x : Fin n → ℝ) ≤ (1 : EReal)} have hEq : closure A = B := section16_closure_sublevel_eq_sublevel_convexFunctionClosure_one (n := n) (h := h) hh hInf have hEq' : closure (e '' A) = e '' B := by have hEq'' : (e.toHomeomorph) '' closure A = (e.toHomeomorph) '' B := by simpa using congrArg (fun S => (e.toHomeomorph) '' S) hEq have hcl : (e.toHomeomorph) '' closure A = closure ((e.toHomeomorph) '' A) := by simpa using (Homeomorph.image_closure (h := e.toHomeomorph) (s := A)) have hEq''' : closure ((e.toHomeomorph) '' A) = (e.toHomeomorph) '' B := by calc closure ((e.toHomeomorph) '' A) = (e.toHomeomorph) '' closure A := by simpa using hcl.symm _ = (e.toHomeomorph) '' B := hEq'' simpa using hEq''' have hA : e '' A = {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} := by ext xStar constructor · rintro ⟨x, hx, rfl⟩ simpa [A] using hx · intro hx refine ⟨e.symm xStar, ?_, by simp [e]⟩ simpa [A, e] using hx have hB : e '' B = {xStar : Fin n → ℝ | convexFunctionClosure h xStar ≤ (1 : EReal)} := by ext xStar constructor · rintro ⟨x, hx, rfl⟩ simpa [B] using hx · intro hx refine ⟨e.symm xStar, ?_, by simp [e]⟩ simpa [B, e] using hx simpa [hA, hB] using hEq'

The support function of a nonempty convex set agrees with that of its closure.

lemma section16_supportFunctionEReal_eq_supportFunctionEReal_closure {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hCne : C.Nonempty) : supportFunctionEReal C = supportFunctionEReal (closure C) := by calc supportFunctionEReal C = fenchelConjugate n (indicatorFunction C) := by symm exact section13_fenchelConjugate_indicatorFunction_eq_supportFunctionEReal (C := C) _ = fenchelConjugate n (convexFunctionClosure (indicatorFunction C)) := by symm exact (fenchelConjugate_eq_of_convexFunctionClosure (n := n) (f := indicatorFunction C)) _ = fenchelConjugate n (indicatorFunction (closure C)) := by simp [section16_convexFunctionClosure_indicatorFunction_eq_indicatorFunction_closure, hC, hCne] _ = supportFunctionEReal (closure C) := by exact section13_fenchelConjugate_indicatorFunction_eq_supportFunctionEReal (C := closure C)

The support function is nonnegative when 0 : ℕ0 lies in the closure.

lemma section16_supportFunctionEReal_nonneg_of_zero_mem_closure {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hCne : C.Nonempty) (h0 : (0 : Fin n → ℝ) ∈ closure C) (xStar : Fin n → ℝ) : (0 : EReal) ≤ supportFunctionEReal C xStar := by have hmem : (0 : EReal) ∈ {z : EReal | ∃ x ∈ closure C, z = ((dotProduct x xStar : ℝ) : EReal)} := by refine ⟨0, h0, ?_⟩ simp have hnonneg_closure : (0 : EReal) ≤ supportFunctionEReal (closure C) xStar := by unfold supportFunctionEReal exact le_sSup hmem have hEq := section16_supportFunctionEReal_eq_supportFunctionEReal_closure (C := C) hC hCne simpa [hEq] using hnonneg_closure

Points in the sublevel of the hull lie in the closure of the convex hull of the sublevels.

lemma section16_mem_closure_convexHull_iUnion_sublevels_of_hle_one {n : ℕ} {ι : Sort _} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ i, Convex ℝ (C i)) (hCne : ∀ i, (C i).Nonempty) (h0 : ∀ i, (0 : Fin n → ℝ) ∈ closure (C i)) {xStar : Fin n → ℝ} (hle : convexHullFunctionFamily (fun i => supportFunctionEReal (C i)) xStar ≤ (1 : EReal)) : xStar ∈ closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | supportFunctionEReal (C i) xStar ≤ (1 : EReal)})) := by classical let g : ι → (Fin n → ℝ) → EReal := fun i => supportFunctionEReal (C i) let K : Set (Fin n → ℝ) := convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)}) have hpos : ∀ i, PositivelyHomogeneous (g i) := by intro i exact (section13_supportFunctionEReal_closedProperConvex_posHom (n := n) (C := C i) (hCne i) (hC i)).2.2 have hnonneg : ∀ i x, (0 : EReal) ≤ g i x := by intro i x have hnonneg' := section16_supportFunctionEReal_nonneg_of_zero_mem_closure (C := C i) (hC i) (hCne i) (h0 i) x simpa [g] using hnonneg' have hmemK : ∀ ε : ℝ, ε > 0 → ((1 + ε)⁻¹) • xStar ∈ closure K := by intro ε hε obtain ⟨μ, hμlt, hmem⟩ := section16_exists_mem_convexHull_union_epigraph_lt_one_add_eps_of_hle_one (g := g) (xStar := xStar) (ε := ε) hε (by simpa [g] using hle) have hmem' : (xStar, 1 + ε) ∈ convexHull ℝ (⋃ i, epigraph (S := (Set.univ : Set (Fin n → ℝ))) (g i)) := by refine section16_convexHull_union_epigraph_mono_snd (g := g) (x := xStar) (μ := μ) (μ' := 1 + ε) hmem ?_ linarith have hnorm : ((1 + ε)⁻¹) • xStar ∈ closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)})) := by exact section16_mem_convexHull_iUnion_sublevels_one_of_mem_convexHull_union_epigraph_one_add_eps (g := g) hpos hnonneg hε hmem' simpa [K] using hnorm have hlim : Tendsto (fun ε : ℝ => ((1 + ε)⁻¹) • xStar) (𝓝[>] (0 : ℝ)) (𝓝 xStar) := by have hcont_add : ContinuousAt (fun ε : ℝ => (1 + ε)) 0 := by simpa using (continuousAt_const.add continuousAt_id) have hcont_inv' : ContinuousAt (fun t : ℝ => t⁻¹) ((1 : ℝ) + 0) := by have hne : ((1 : ℝ) + 0) ≠ 0 := by simp exact continuousAt_inv₀ hne have hcont_inv : ContinuousAt (fun ε : ℝ => (1 + ε)⁻¹) 0 := hcont_inv'.comp hcont_add have hcont : ContinuousAt (fun ε : ℝ => ((1 + ε)⁻¹) • xStar) 0 := hcont_inv.smul continuousAt_const have hlim0 : Tendsto (fun ε : ℝ => ((1 + ε)⁻¹) • xStar) (𝓝 (0 : ℝ)) (𝓝 xStar) := by simpa using hcont.tendsto exact hlim0.mono_left nhdsWithin_le_nhds have hmem_event : ∀ᶠ ε in (𝓝[>] (0 : ℝ)), ((1 + ε)⁻¹) • xStar ∈ closure K := by have hpos_event : ∀ᶠ ε in (𝓝[>] (0 : ℝ)), ε ∈ Ioi (0 : ℝ) := self_mem_nhdsWithin refine hpos_event.mono ?_ intro ε hε have hε' : 0 < ε := by simpa using hε exact hmemK ε hε' have hxStar : xStar ∈ closure (closure K) := mem_closure_of_tendsto hlim hmem_event have hxStar' : xStar ∈ closure K := by simpa [closure_closure] using hxStar simpa [K, g] using hxStar'

The sublevel of the convex-hull support family has the same closure as the convex hull of the sublevels of the family.

lemma section16_closure_sublevel_convexHullFunctionFamily_supportFamily_one_eq_closure_convexHull_iUnion_sublevels {n : ℕ} {ι : Sort _} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ i, Convex ℝ (C i)) (hCne : ∀ i, (C i).Nonempty) (h0 : ∀ i, (0 : Fin n → ℝ) ∈ closure (C i)) : let g : ι → (Fin n → ℝ) → EReal := fun i => supportFunctionEReal (C i) let h := convexHullFunctionFamily g closure {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} = closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)})) := by classical let g : ι → (Fin n → ℝ) → EReal := fun i => supportFunctionEReal (C i) let h := convexHullFunctionFamily g have hgoal : closure {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} = closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)})) := by have hminor : ConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) h ∧ (∀ i, h ≤ g i) ∧ ∀ h' : (Fin n → ℝ) → EReal, ConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) h' → (∀ i, h' ≤ g i) → h' ≤ h := by simpa [h] using (convexHullFunctionFamily_greatest_convex_minorant (f := g)) have hconvfun : ConvexFunction h := by simpa [ConvexFunction] using hminor.1 have hconvset : Convex ℝ {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} := by have hlevel := (convexFunction_level_sets_convex (f := h) hconvfun (1 : EReal)) exact hlevel.2 have hsubset : (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)}) ⊆ {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} := by intro x hx rcases Set.mem_iUnion.1 hx with ⟨i, hi⟩ have hle : h x ≤ g i x := (hminor.2.1 i) x exact le_trans hle (by simpa using hi) have hsubset_conv : convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)}) ⊆ {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} := by exact convexHull_min hsubset hconvset have hclosure : closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)})) ⊆ closure {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} := by exact closure_mono hsubset_conv refine le_antisymm ?_ ?_ · have hsubset' : {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} ⊆ closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)})) := by intro xStar hx have hx' : xStar ∈ closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | supportFunctionEReal (C i) xStar ≤ (1 : EReal)})) := by simpa [g, h] using (section16_mem_closure_convexHull_iUnion_sublevels_of_hle_one (C := C) hC hCne h0 (xStar := xStar) (by simpa [h] using hx)) simpa [g] using hx' have hclosure' : closure {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} ⊆ closure (closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)}))) := closure_mono hsubset' simpa [closure_closure] using hclosure' · exact hclosure simpa [g, h] using hgoal

Corollary 16.5.2.2: Let Unknown identifier `C`C i be a convex set in ℝ ^ sorry : Typeℝ^Unknown identifier `n`n for each Unknown identifier `i`i in a nonempty index set, assume the intersection of the closures is nonempty, and that this intersection contains 0 : ℕ0. Then

.

In this development, the polar of a set Unknown identifier `S`S is represented by {xStar | ∀ x ∈ sorry, x ⬝ᵥ xStar ≤ 1} : Set (?m.13 → ℝ){xStar | ∀ x ∈ Unknown identifier `S`S, (dotProduct x xStar : ℝ) ≤ 1}.

theorem section16_polar_iInter_closure_eq_closure_convexHull_iUnion_polars {n : ℕ} {ι : Sort _} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ i, Convex ℝ (C i)) (h0 : (0 : Fin n → ℝ) ∈ ⋂ i, closure (C i)) (hInter : (⋂ i, closure (C i)).Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ (⋂ i, closure (C i)), (dotProduct x xStar : ℝ) ≤ 1} = closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | ∀ x ∈ C i, (dotProduct x xStar : ℝ) ≤ 1})) := by classical have hCne : ∀ i, (C i).Nonempty := by intro i rcases hInter with ⟨x0, hx0⟩ have hx0i : x0 ∈ closure (C i) := (Set.mem_iInter.1 hx0 i) by_contra hne have hCi : C i = ∅ := Set.not_nonempty_iff_eq_empty.1 hne simp [hCi] at hx0i have h0i : ∀ i, (0 : Fin n → ℝ) ∈ closure (C i) := by intro i exact (Set.mem_iInter.1 h0 i) let g : ι → (Fin n → ℝ) → EReal := fun i => supportFunctionEReal (C i) let h := convexHullFunctionFamily g have hpolar : {xStar : Fin n → ℝ | ∀ x ∈ (⋂ i, closure (C i)), (dotProduct x xStar : ℝ) ≤ 1} = {xStar : Fin n → ℝ | supportFunctionEReal (⋂ i, closure (C i)) xStar ≤ (1 : EReal)} := by simpa using (section16_polar_eq_sublevel_deltaStar (C := ⋂ i, closure (C i))) have hsupport : supportFunctionEReal (⋂ i, closure (C i)) = convexFunctionClosure h := by simpa [h] using (section16_supportFunctionEReal_iInter_closure_eq_convexFunctionClosure_convexHullFunctionFamily (C := C) hC hCne) have hproper : ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) h ∧ iInf (fun xStar => h xStar) < (1 : EReal) := by simpa [g, h] using (section16_properConvexFunctionOn_convexHullFunctionFamily_supportFamily_of_exists_common_point (C := C) hC hInter) have hsub : {xStar : Fin n → ℝ | convexFunctionClosure h xStar ≤ (1 : EReal)} = closure {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} := by simpa using (section16_closure_sublevel_eq_sublevel_convexFunctionClosure_one_fin (h := h) hproper.1 hproper.2).symm have hsublevels : (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)}) = (⋃ i, {xStar : Fin n → ℝ | ∀ x ∈ C i, (dotProduct x xStar : ℝ) ≤ 1}) := by ext xStar constructor · intro hx rcases Set.mem_iUnion.1 hx with ⟨i, hx⟩ have hx' : xStar ∈ {xStar : Fin n → ℝ | supportFunctionEReal (C i) xStar ≤ (1 : EReal)} := by simpa [g] using hx have hx'' : xStar ∈ {xStar : Fin n → ℝ | ∀ x ∈ C i, (dotProduct x xStar : ℝ) ≤ 1} := by simpa [(section16_polar_eq_sublevel_deltaStar (C := C i)).symm] using hx' exact Set.mem_iUnion.2 ⟨i, hx''⟩ · intro hx rcases Set.mem_iUnion.1 hx with ⟨i, hx⟩ have hx' : xStar ∈ {xStar : Fin n → ℝ | supportFunctionEReal (C i) xStar ≤ (1 : EReal)} := by simpa [section16_polar_eq_sublevel_deltaStar (C := C i)] using hx have hx'' : xStar ∈ {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)} := by simpa [g] using hx' exact Set.mem_iUnion.2 ⟨i, hx''⟩ calc {xStar : Fin n → ℝ | ∀ x ∈ (⋂ i, closure (C i)), (dotProduct x xStar : ℝ) ≤ 1} = {xStar : Fin n → ℝ | supportFunctionEReal (⋂ i, closure (C i)) xStar ≤ (1 : EReal)} := hpolar _ = {xStar : Fin n → ℝ | convexFunctionClosure h xStar ≤ (1 : EReal)} := by simp [hsupport] _ = closure {xStar : Fin n → ℝ | h xStar ≤ (1 : EReal)} := hsub _ = closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | g i xStar ≤ (1 : EReal)})) := by simpa [g, h] using (section16_closure_sublevel_convexHullFunctionFamily_supportFamily_one_eq_closure_convexHull_iUnion_sublevels (C := C) hC hCne h0i) _ = closure (convexHull ℝ (⋃ i, {xStar : Fin n → ℝ | ∀ x ∈ C i, (dotProduct x xStar : ℝ) ≤ 1})) := by simp [hsublevels]

A common relative-interior point yields finite iSup.{u, v} {α : Type u} {ι : Sort v} [SupSet α] (s : ι → α) : αiSup for a finite family.

lemma section16_exists_common_ri_point_finite_iSup_ne_top_of_common_closure_effectiveDomain {n : ℕ} {ι : Type _} [Fintype ι] [Nonempty ι] (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ i, ProperConvexFunctionOn (Set.univ : Set (Fin n → ℝ)) (f i)) (C : Set (Fin n → ℝ)) (hC : ∀ i, closure (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i)) = C) : ∃ x0 : EuclideanSpace ℝ (Fin n), (∀ i, x0 ∈ euclideanRelativeInterior n (Set.image (EuclideanSpace.equiv (Fin n) ℝ).symm (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i)))) ∧ (iSup (fun i => f i ((EuclideanSpace.equiv (Fin n) ℝ) x0))) ≠ (⊤ : EReal) := by classical obtain ⟨i0⟩ := (inferInstance : Nonempty ι) let e := (EuclideanSpace.equiv (Fin n) ℝ) let domE : ι → Set (EuclideanSpace ℝ (Fin n)) := fun i => Set.image e.symm (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i)) let CE : Set (EuclideanSpace ℝ (Fin n)) := Set.image e.symm C have hconv_dom : ∀ i, Convex ℝ (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i)) := by intro i exact effectiveDomain_convex (S := (Set.univ : Set (Fin n → ℝ))) (f := f i) (hf i).1 have hconv_domE : ∀ i, Convex ℝ (domE i) := by intro i exact (hconv_dom i).linear_image e.symm.toLinearMap have hne_dom : ∀ i, (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i)).Nonempty := by intro i exact section13_effectiveDomain_nonempty_of_proper (n := n) (f := f i) (hf i) have hconv_C : Convex ℝ C := by have hconv0 : Convex ℝ (closure (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i0))) := (hconv_dom i0).closure simpa [hC i0] using hconv0 have hconv_CE : Convex ℝ CE := by exact hconv_C.linear_image e.symm.toLinearMap have hCne : C.Nonempty := by have hne0 : (closure (effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i0))).Nonempty := (hne_dom i0).closure simpa [hC i0] using hne0 have hCEne : CE.Nonempty := by rcases hCne with ⟨x, hx⟩ exact ⟨e.symm x, ⟨x, hx, rfl⟩⟩ have hcl_domE : ∀ i, closure (domE i) = CE := by intro i have hcl := (e.symm.toHomeomorph.image_closure (s := effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i))).symm simpa [domE, CE, hC i] using hcl have hCE_closed : IsClosed CE := by have hcl0 : closure (domE i0) = CE := hcl_domE i0 simpa [hcl0] using (isClosed_closure : IsClosed (closure (domE i0))) obtain ⟨x0, hx0C⟩ : (euclideanRelativeInterior n CE).Nonempty := (euclideanRelativeInterior_closure_convex_affineSpan n CE hconv_CE).2.2.2.2 hCEne have hri_eq : ∀ i, euclideanRelativeInterior n (domE i) = euclideanRelativeInterior n CE := by intro i have hcl' : closure (domE i) = closure CE := by calc closure (domE i) = CE := hcl_domE i _ = closure CE := by simp exact euclideanRelativeInterior_eq_of_closure_eq n (domE i) CE (hconv_domE i) hconv_CE hcl' have hx0ri : ∀ i, x0 ∈ euclideanRelativeInterior n (domE i) := by intro i simpa [hri_eq i] using hx0C have hx0_dom : ∀ i, (e x0) ∈ effectiveDomain (Set.univ : Set (Fin n → ℝ)) (f i) := by intro i have hx0_mem : x0 ∈ domE i := (euclideanRelativeInterior_subset_closure n (domE i)).1 (hx0ri i) rcases hx0_mem with ⟨x', hx', hx0_eq⟩ have hx_eq : x' = e x0 := by simpa using congrArg e hx0_eq simpa [hx_eq] using hx' have hlt_top : iSup (fun i => f i (e x0)) < (⊤ : EReal) := by let eFin : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι have hm : 0 < Fintype.card ι := by simpa using (Fintype.card_pos_iff.mpr (inferInstance : Nonempty ι)) have hlt' : iSup (fun k : Fin (Fintype.card ι) => f (eFin.symm k) (e x0)) < (⊤ : EReal) := by refine iSup_lt_of_forall_lt_fin (m := Fintype.card ι) (r := (⊤ : EReal)) hm ?_ intro k have hx0_lt : f (eFin.symm k) (e x0) < (⊤ : EReal) := by have hx0' : (e x0) ∈ (Set.univ : Set (Fin n → ℝ)) ∧ f (eFin.symm k) (e x0) < (⊤ : EReal) := by simpa [effectiveDomain_eq] using (hx0_dom (eFin.symm k)) exact hx0'.2 exact hx0_lt have hcongr : iSup (fun i : ι => f i (e x0)) = iSup (fun k : Fin (Fintype.card ι) => f (eFin.symm k) (e x0)) := by refine (Equiv.iSup_congr eFin ?_) intro i simp simpa [hcongr] using hlt' exact ⟨x0, hx0ri, ne_of_lt hlt_top⟩