theorem section16_properConvexFunctionOn_indicatorFunction_univ {n : ℕ} {C : Set (Fin n → ℝ)} (hC : Convex ℝ C) (hCne : C.Nonempty) : ProperConvexFunctionOn Set.univ (indicatorFunction C)

The indicator function of a nonempty convex set is proper convex on Set.univ.

theorem section16_convexHullFunctionFamily_indicatorFunction_eq_indicatorFunction_convexHull_iUnion {n : ℕ} {ι : Sort u_1} (C : ι → Set (Fin n → ℝ)) : (convexHullFunctionFamily fun (i : ι) => indicatorFunction (C i)) = indicatorFunction ((convexHull ℝ) (⋃ (i : ι), C i))

The convex hull of indicator functions is the indicator of the convex hull of the union.

theorem section16_supportFunctionEReal_convexHull_iUnion {n : ℕ} {ι : Sort u_1} (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) (hCne : ∀ (i : ι), (C i).Nonempty) : supportFunctionEReal ((convexHull ℝ) (⋃ (i : ι), C i)) = fun (xStar : Fin n → ℝ) => sSup (Set.range fun (i : ι) => supportFunctionEReal (C i) xStar)

Support function of the convex hull of a union as a supremum of support functions.

theorem section16_deltaStar_convexHull_iUnion {n : ℕ} {ι : Sort u_1} (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) (hCne : ∀ (i : ι), (C i).Nonempty) : supportFunctionEReal ((convexHull ℝ) (⋃ (i : ι), C i)) = fun (xStar : Fin n → ℝ) => sSup (Set.range fun (i : ι) => supportFunctionEReal (C i) xStar)

Corollary 16.5.1.1: Let C i be a non-empty convex set in ℝⁿ for each i in an index set. Let D be the convex hull of the union ⋃ i, C i. Then the support function satisfies

δ^*(· | D) = sup { δ^*(· | C i) | i },

where δ^*(· | C) is represented by supportFunctionEReal C.

theorem section16_fenchelConjugate_convexHullFunctionFamily_fenchelConjugate_eq_sSup_convexFunctionClosure {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) : fenchelConjugate n (convexHullFunctionFamily fun (i : ι) => fenchelConjugate n (f i)) = fun (x : Fin n → ℝ) => sSup (Set.range fun (i : ι) => convexFunctionClosure (f i) x)

Applying Theorem 16.5.1 to the family of conjugates yields the supremum of closures.

theorem section16_convexFunction_convexHullFunctionFamily_fenchelConjugate {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) : ConvexFunction (convexHullFunctionFamily fun (i : ι) => fenchelConjugate n (f i))

The convex hull of the conjugate family is a convex function.

theorem section16_fenchelConjugate_sSup_convexFunctionClosure_eq_via_biconjugate {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) : (fenchelConjugate n fun (x : Fin n → ℝ) => sSup (Set.range fun (i : ι) => convexFunctionClosure (f i) x)) = convexFunctionClosure (convexHullFunctionFamily fun (i : ι) => fenchelConjugate n (f i))

The conjugate of the supremum of closures is the closure of the convex hull of conjugates.

theorem section16_fenchelConjugate_sSup_convexFunctionClosure_eq_convexFunctionClosure_convexHullFunctionFamily {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) : (fenchelConjugate n fun (x : Fin n → ℝ) => sSup (Set.range fun (i : ι) => convexFunctionClosure (f i) x)) = convexFunctionClosure (convexHullFunctionFamily fun (i : ι) => fenchelConjugate n (f i))

Theorem 16.5.2: Let f i be a proper convex function on ℝ^n for each i in an (arbitrary) index set. Then the Fenchel conjugate of the pointwise supremum of the closures cl f_i is the closure of the convex hull of the conjugates:

(sup {cl f_i | i ∈ I})^* = cl (conv {f_i^* | i ∈ I}).

Here cl is the convex-function closure convexFunctionClosure, sup is modeled pointwise by x ↦ sSup (range fun i => ·), conv is convexHullFunctionFamily, and f_i^* is fenchelConjugate n (f i).

theorem section16_sSup_range_indicatorFunction_closure_eq_indicatorFunction_iInter_closure {n : ℕ} {ι : Sort u_1} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) : (fun (x : Fin n → ℝ) => sSup (Set.range fun (i : ι) => indicatorFunction (closure (C i)) x)) = indicatorFunction (⋂ (i : ι), closure (C i))

Pointwise supremum of indicator functions of closures is the indicator of the intersection.

theorem section16_supportFunctionEReal_iInter_closure_eq_convexFunctionClosure_convexHullFunctionFamily {n : ℕ} {ι : Sort u_1} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) (hCne : ∀ (i : ι), (C i).Nonempty) : supportFunctionEReal (⋂ (i : ι), closure (C i)) = convexFunctionClosure (convexHullFunctionFamily fun (i : ι) => supportFunctionEReal (C i))

Support function of the intersection of closures as a convex hull closure.

theorem section16_supportFunctionEReal_iInter_closure_eq_convexFunctionClosure_convexHullFunctionFamily_and_convexHull_iUnion {n : ℕ} {ι : Sort u_1} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) (hCne : ∀ (i : ι), (C i).Nonempty) : have C' := ⋂ (i : ι), closure (C i); have D := (convexHull ℝ) (⋃ (i : ι), C i); supportFunctionEReal C' = convexFunctionClosure (convexHullFunctionFamily fun (i : ι) => supportFunctionEReal (C i)) ∧ supportFunctionEReal D = fun (xStar : Fin n → ℝ) => sSup (Set.range fun (i : ι) => supportFunctionEReal (C i) xStar)

Corollary 16.5.1.2: Let C i be a non-empty convex set in ℝ^n for each i in an index set. Let C be the intersection ⋂ i, closure (C i). Then the support function satisfies

δ^*(· | C) = cl (conv { δ^*(· | C i) | i }).

Moreover,

δ^*(· | D) = sup { δ^*(· | C i) | i }.

In this development, δ^* is supportFunctionEReal, cl is convexFunctionClosure, and conv is convexHullFunctionFamily.

theorem section16_convex_set_dotProduct_le_one {n : ℕ} (xStar : Fin n → ℝ) : Convex ℝ {x : Fin n → ℝ | x ⬝ᵥ xStar ≤ 1}

The sublevel set {x | dotProduct x xStar ≤ 1} is convex.

theorem section16_polar_convexHull_iUnion_subset_iInter_polars {n : ℕ} {ι : Sort u_1} (C : ι → Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (h : ∀ x ∈ (convexHull ℝ) (⋃ (i : ι), C i), x ⬝ᵥ xStar ≤ 1) (i : ι) (x : Fin n → ℝ) : x ∈ C i → x ⬝ᵥ xStar ≤ 1

Polar inclusion from the convex hull of a union to the intersection of polars.

theorem section16_iInter_polars_subset_polar_convexHull_iUnion {n : ℕ} {ι : Sort u_1} (C : ι → Set (Fin n → ℝ)) (xStar : Fin n → ℝ) (h : ∀ (i : ι), ∀ x ∈ C i, x ⬝ᵥ xStar ≤ 1) (x : Fin n → ℝ) : x ∈ (convexHull ℝ) (⋃ (i : ι), C i) → x ⬝ᵥ xStar ≤ 1

Polar inclusion from the intersection of polars to the polar of the convex hull of a union.

theorem section16_polar_convexHull_iUnion_eq_iInter_polars {n : ℕ} {ι : Sort u_1} (C : ι → Set (Fin n → ℝ)) : {xStar : Fin n → ℝ | ∀ x ∈ (convexHull ℝ) (⋃ (i : ι), C i), x ⬝ᵥ xStar ≤ 1} = ⋂ (i : ι), {xStar : Fin n → ℝ | ∀ x ∈ C i, x ⬝ᵥ xStar ≤ 1}

Corollary 16.5.2.1: Let C i be a convex set in ℝ^n for each i in an index set. Then the polar of the convex hull of the family equals the intersection of the polars:

(conv { C_i | i ∈ I })^∘ = ⋂ { C_i^∘ | i ∈ I }.

In this development, conv { C_i | i ∈ I } is represented by convexHull ℝ (⋃ i, C i), and the polar of a set S is represented by {xStar | ∀ x ∈ S, (dotProduct x xStar : ℝ) ≤ 1}.

theorem section16_properConvexFunctionOn_convexHullFunctionFamily_supportFamily_of_exists_common_point {n : ℕ} {ι : Sort u_1} [Nonempty ι] (C : ι → Set (Fin n → ℝ)) (hC : ∀ (i : ι), Convex ℝ (C i)) (hInter : (⋂ (i : ι), closure (C i)).Nonempty) : have g := fun (i : ι) => supportFunctionEReal (C i); have h := convexHullFunctionFamily g; ProperConvexFunctionOn Set.univ h ∧ ⨅ (xStar : Fin n → ℝ), h xStar < 1

A common point in the intersection of closures yields a proper convex hull of support functions with a finite ≤ 1 sublevel.

theorem section16_convexHull_union_epigraph_mono_snd {n : ℕ} {ι : Sort u_1} {g : ι → (Fin n → ℝ) → EReal} {x : Fin n → ℝ} {μ μ' : ℝ} (hmem : (x, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (g i))) (hle : μ ≤ μ') : (x, μ') ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (g i))

Raising the second coordinate preserves membership in the convex hull of a union of epigraphs.

theorem section16_exists_mem_convexHull_union_epigraph_lt_one_add_eps_of_hle_one {n : ℕ} {ι : Sort u_1} (g : ι → (Fin n → ℝ) → EReal) {xStar : Fin n → ℝ} {ε : ℝ} (hε : 0 < ε) (hle : convexHullFunctionFamily g xStar ≤ 1) : ∃ μ < 1 + ε, (xStar, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (g i))

A small epigraph height above 1 appears in the convex hull of the union of epigraphs.

theorem section16_epigraph_univ_posHom_smul_mem {n : ℕ} {g : (Fin n → ℝ) → EReal} (hpos : PositivelyHomogeneous g) {x : Fin n → ℝ} {μ t : ℝ} (ht : 0 < t) (hmem : (x, μ) ∈ epigraph Set.univ g) : (t • x, t * μ) ∈ epigraph Set.univ g

Positive homogeneity scales epigraph points.

theorem section16_convexHull_union_epigraph_smul_mem {n : ℕ} {ι : Sort u_1} {g : ι → (Fin n → ℝ) → EReal} (hpos : ∀ (i : ι), PositivelyHomogeneous (g i)) {x : Fin n → ℝ} {μ t : ℝ} (ht : 0 < t) (hmem : (x, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (g i))) : (t • x, t * μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (g i))

Scaling preserves membership in the convex hull of a union of epigraphs.

theorem section16_closedConvex_closure_convexHull_iUnion_sublevels {n : ℕ} {ι : Sort u_1} {g : ι → (Fin n → ℝ) → EReal} : IsClosed (closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | g i xStar ≤ 1}))) ∧ Convex ℝ (closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | g i xStar ≤ 1})))

Closedness and convexity of the closure of the convex hull of level-1 sublevels.

theorem section16_exists_sep_clm_of_not_mem_closure_convexHull_iUnion_sublevels {n : ℕ} {ι : Sort u_1} {g : ι → (Fin n → ℝ) → EReal} {xStar : Fin n → ℝ} (hx : xStar ∉ closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | g i xStar ≤ 1}))) : ∃ (φ : (Fin n → ℝ) →L[ℝ] ℝ) (u : ℝ), (∀ y ∈ closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | g i xStar ≤ 1})), φ y ≤ u) ∧ u < φ xStar

A separating continuous linear functional for a point outside the closed convex hull.

theorem section16_clm_le_mul_snd_of_mem_epigraph_of_pos {n : ℕ} {ι : Sort u_1} {g : ι → (Fin n → ℝ) → EReal} {i : ι} (hpos : PositivelyHomogeneous (g i)) {φ : (Fin n → ℝ) →L[ℝ] ℝ} {u : ℝ} (hbound : ∀ (z : Fin n → ℝ), g i z ≤ 1 → φ z ≤ u) {x : Fin n → ℝ} {μ : ℝ} (hmem : (x, μ) ∈ epigraph Set.univ (g i)) (hμ : 0 < μ) : φ x ≤ u * μ

A separator bounded on the level-1 sublevel controls positive-height epigraph points.

theorem section16_slice_one_convexHull_union_epigraph_subset_closure_convexHull_sublevels {n : ℕ} {ι : Sort u_1} {g : ι → (Fin n → ℝ) → EReal} (hpos : ∀ (i : ι), PositivelyHomogeneous (g i)) (hnonneg : ∀ (i : ι) (x : Fin n → ℝ), 0 ≤ g i x) : {xStar : Fin n → ℝ | (xStar, 1) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (g i))} ⊆ closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | g i xStar ≤ 1}))

The μ = 1 slice of a convex hull of epigraphs lies in the closure of the hull of slices.

theorem section16_mem_convexHull_iUnion_sublevels_one_of_mem_convexHull_union_epigraph_one_add_eps {n : ℕ} {ι : Sort u_1} {g : ι → (Fin n → ℝ) → EReal} (hpos : ∀ (i : ι), PositivelyHomogeneous (g i)) (hnonneg : ∀ (i : ι) (x : Fin n → ℝ), 0 ≤ g i x) {xStar : Fin n → ℝ} {ε : ℝ} (hε : 0 < ε) (hmem : (xStar, 1 + ε) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (g i))) : (1 + ε)⁻¹ • xStar ∈ closure ((convexHull ℝ) (⋃ (i : ι), {xStar : Fin n → ℝ | g i xStar ≤ 1}))

Normalize a convex-hull epigraph point at height 1 + ε to the level-1 sublevel hull, landing in the closure.