theorem convexHullFunction_eq_sInf_convexCombination {n : ℕ} {g : (Fin n → ℝ) → EReal} (h_not_bot : ∀ (x : Fin n → ℝ), g x ≠ ⊥) (x : Fin n → ℝ) : convexHullFunction g x = sInf {z : EReal | ∃ (m : ℕ) (lam : Fin m → ℝ) (x' : Fin m → Fin n → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ ∑ i : Fin m, lam i • x' i = x ∧ z = ∑ i : Fin m, ↑(lam i) * g (x' i)}

Text 5.5.4: conv(g)(x) = inf { λ_1 g(x_1) + ... + λ_m g(x_m) | λ_1 x_1 + ... + λ_m x_m = x }, where the infimum is taken over all convex combinations of points of ℝ^n, assuming g never takes the value -∞.

noncomputable def convexHullFunctionFamily {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Text 5.5.5: The convex hull of an arbitrary collection of functions {f_i | i ∈ I} on ℝ^n is denoted conv {f_i | i ∈ I}. It is the function obtained via Theorem 5.3 from the convex hull of the union of the epigraphs of the f_i.

Equations

• convexHullFunctionFamily f x = sInf ((fun (μ : ℝ) => ↑μ) '' {μ : ℝ | (x, μ) ∈ (convexHull ℝ) (⋃ (i : ι), epigraph Set.univ (f i))})