Bridging EuclideanSpace sublevel-closure to Fin n → ℝ

theorem section16_closure_sublevel_eq_sublevel_convexFunctionClosure_one_fin {n : ℕ} {h : (Fin n → ℝ) → EReal} (hh : ProperConvexFunctionOn Set.univ h) (hInf : ⨅ (x : Fin n → ℝ), h x < 1) : closure {xStar : Fin n → ℝ | h xStar ≤ 1} = {xStar : Fin n → ℝ | convexFunctionClosure h xStar ≤ 1}

Closure of a ≤ 1 sublevel set matches the ≤ 1 sublevel of the convex-function closure when the domain is Fin n → ℝ.

theorem section16_supportFunctionEReal_eq_supportFunctionEReal_closure {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hCne : C.Nonempty) : supportFunctionEReal C = supportFunctionEReal (closure C)

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

theorem section16_supportFunctionEReal_nonneg_of_zero_mem_closure {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hCne : C.Nonempty) (h0 : 0 ∈ closure C) (xStar : Fin n → ℝ) : 0 ≤ supportFunctionEReal C xStar

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

theorem section16_mem_closure_convexHull_iUnion_sublevels_of_hle_one {n : ℕ} {ι : Sort u_1} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) (hCne : ∀ (i : ι), (C i).Nonempty) (h0 : ∀ (i : ι), 0 ∈ closure (C i)) {xStar : Fin n → ℝ} (hle : convexHullFunctionFamily (fun (i : ι) => supportFunctionEReal (C i)) xStar ≤ 1) : xStar ∈ closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | supportFunctionEReal (C i) xStar ≤ 1}))

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

theorem section16_closure_sublevel_convexHullFunctionFamily_supportFamily_one_eq_closure_convexHull_iUnion_sublevels {n : ℕ} {ι : Sort u_1} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) (hCne : ∀ (i : ι), (C i).Nonempty) (h0 : ∀ (i : ι), 0 ∈ closure (C i)) : have g := fun (i : ι) => supportFunctionEReal (C i); have h := convexHullFunctionFamily g; closure {xStar : Fin n → ℝ | h xStar ≤ 1} = closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | g i xStar ≤ 1}))

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

theorem section16_polar_iInter_closure_eq_closure_convexHull_iUnion_polars {n : ℕ} {ι : Sort u_1} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) (h0 : 0 ∈ ⋂ (i : ι), closure (C i)) (hInter : (⋂ (i : ι), closure (C i)).Nonempty) : {xStar : Fin n → ℝ | ∀ x ∈ ⋂ (i : ι), closure (C i), x ⬝ᵥ xStar ≤ 1} = closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | ∀ x ∈ C i, x ⬝ᵥ xStar ≤ 1}))

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

(⋂ i, closure (C i))^∘ = closure (convexHull ℝ (⋃ i, (C i)^∘)).

In this development, the polar of a set S is represented by {xStar | ∀ x ∈ S, (dotProduct x xStar : ℝ) ≤ 1}.

theorem section16_exists_common_ri_point_finite_iSup_ne_top_of_common_closure_effectiveDomain {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) (C : Set (Fin n → ℝ)) (hC : ∀ (i : ι), closure (effectiveDomain Set.univ (f i)) = C) : ∃ (x0 : EuclideanSpace ℝ (Fin n)), (∀ (i : ι), x0 ∈ euclideanRelativeInterior n (⇑(EuclideanSpace.equiv (Fin n) ℝ).symm '' effectiveDomain Set.univ (f i))) ∧ ⨆ (i : ι), f i ((EuclideanSpace.equiv (Fin n) ℝ) x0) ≠ ⊤

A common relative-interior point yields finite iSup for a finite family.

theorem section16_convexFunctionClosure_iSup_eq_iSup_convexFunctionClosure_of_fintype_of_common_closure_effectiveDomain {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) (C : Set (Fin n → ℝ)) (hC : ∀ (i : ι), closure (effectiveDomain Set.univ (f i)) = C) : (convexFunctionClosure fun (x : Fin n → ℝ) => ⨆ (i : ι), f i x) = fun (x : Fin n → ℝ) => ⨆ (i : ι), convexFunctionClosure (f i) x

Closure commutes with a finite iSup under a common domain closure.

theorem section16_common_recession_fenchelConjugate_of_common_closure_effectiveDomain {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) (C : Set (Fin n → ℝ)) (hC : ∀ (i : ι), closure (effectiveDomain Set.univ (f i)) = C) (i : ι) : recessionFunction (fenchelConjugate n (f i)) = supportFunctionEReal C

Conjugates share a common recession function under a common domain closure.

theorem section16_convexHullFunctionFamily_fenchelConjugate_closed_and_attained_of_common_closure_effectiveDomain {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) (C : Set (Fin n → ℝ)) (hC : ∀ (i : ι), closure (effectiveDomain Set.univ (f i)) = C) : have g := fun (i : ι) => fenchelConjugate n (f i); convexFunctionClosure (convexHullFunctionFamily g) = convexHullFunctionFamily g ∧ ∀ (xStar : Fin n → ℝ), ∃ (lam : ι → ℝ) (xStar_i : ι → Fin n → ℝ), (∀ (i : ι), 0 ≤ lam i) ∧ ∑ i : ι, lam i = 1 ∧ ∑ i : ι, lam i • xStar_i i = xStar ∧ convexHullFunctionFamily g xStar = ∑ i : ι, ↑(lam i) * g i (xStar_i i)

Closedness and attainment for the convex hull of conjugates under common domain closure.

theorem section16_convexHullFunctionFamily_congr_equiv {n : ℕ} {ι : Sort u_1} {κ : Sort u_2} (e : ι ≃ κ) (g : ι → (Fin n → ℝ) → EReal) : (convexHullFunctionFamily fun (k : κ) => g (e.symm k)) = convexHullFunctionFamily g

Reindexing a function family by an equivalence does not change its convex hull.

theorem section16_convexHullFunctionFamily_eq_sInf_convexCombination_univ_fintype {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) (x : Fin n → ℝ) : convexHullFunctionFamily f x = sInf {r : EReal | ∃ (lam : ι → ℝ) (x' : ι → Fin n → ℝ), (∀ (i : ι), 0 ≤ lam i) ∧ ∑ i : ι, lam i = 1 ∧ ∑ i : ι, lam i • x' i = x ∧ r = ∑ i : ι, ↑(lam i) * f i (x' i)}

Convex-combination formula with full-index sums on a finite index type.

theorem section16_fenchelConjugate_sSup_eq_convexHullFunctionFamily_of_finite_of_closure_effectiveDomain_eq {n : ℕ} {ι : Type u_1} [Fintype ι] [Nonempty ι] (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) (C : Set (Fin n → ℝ)) (hC : ∀ (i : ι), closure (effectiveDomain Set.univ (f i)) = C) : ((fenchelConjugate n fun (x : Fin n → ℝ) => sSup (Set.range fun (i : ι) => f i x)) = convexHullFunctionFamily fun (i : ι) => fenchelConjugate n (f i)) ∧ ∀ (xStar : Fin n → ℝ), have S := {r : EReal | ∃ (lam : ι → ℝ) (xStar_i : ι → Fin n → ℝ), (∀ (i : ι), 0 ≤ lam i) ∧ ∑ i : ι, lam i = 1 ∧ ∑ i : ι, lam i • xStar_i i = xStar ∧ r = ∑ i : ι, ↑(lam i) * fenchelConjugate n (f i) (xStar_i i)}; fenchelConjugate n (fun (x : Fin n → ℝ) => sSup (Set.range fun (i : ι) => f i x)) xStar = sInf S ∧ ∃ r ∈ S, sInf S = r

Theorem 16.5.3: Let f i be a proper convex function on ℝ^n for each i in a finite index set. If the sets cl (dom f i) are all the same set C, then

(supᵢ f i)^* = conv { (f i)^* | i }.

Moreover, for each xStar, (supᵢ f i)^*(xStar) can be expressed as the infimum of ∑ i, λ i * (f i)^*(xStarᵢ) over all representations of xStar as a convex combination xStar = ∑ i, λ i • xStarᵢ, and this infimum is attained. Here dom f i is modeled by effectiveDomain univ (f i) and cl denotes topological closure of sets.