theorem sInf_convexCombination_indicator_eq {n : ℕ} {ι : Type u_1} (a : ι → Fin n → ℝ) (alpha : ι → ℝ) (x : Fin n → ℝ) : sInf {z : EReal | ∃ (s : Finset ι) (lam : ι → ℝ) (x' : ι → Fin n → ℝ), (∀ (i : ι), 0 ≤ lam i) ∧ (∀ i ∉ s, lam i = 0) ∧ ∑ i ∈ s, lam i = 1 ∧ ∑ i ∈ s, lam i • x' i = x ∧ z = ∑ i ∈ s, ↑(lam i) * (indicatorFunction {a i} (x' i) + ↑(alpha i))} = sInf {z : EReal | ∃ (s : Finset ι) (lam : ι → ℝ), (∀ (i : ι), 0 ≤ lam i) ∧ (∀ i ∉ s, lam i = 0) ∧ ∑ i ∈ s, lam i = 1 ∧ ∑ i ∈ s, lam i • a i = x ∧ z = ∑ i ∈ s, ↑(lam i) * ↑(alpha i)}

The sInf formula for indicator-plus-constant functions reduces to coefficients of alpha.

theorem convexHullFunctionFamily_indicator_add_const {n : ℕ} {ι : Type u_1} (a : ι → Fin n → ℝ) (alpha : ι → ℝ) : have f := convexHullFunctionFamily fun (i : ι) (x : Fin n → ℝ) => indicatorFunction {a i} x + ↑(alpha i); (ConvexFunctionOn Set.univ f ∧ (∀ (i : ι), f (a i) ≤ ↑(alpha i)) ∧ ∀ (h : (Fin n → ℝ) → EReal), ConvexFunctionOn Set.univ h → (∀ (i : ι), h (a i) ≤ ↑(alpha i)) → h ≤ f) ∧ ∀ (x : Fin n → ℝ), f x = sInf {z : EReal | ∃ (s : Finset ι) (lam : ι → ℝ), (∀ (i : ι), 0 ≤ lam i) ∧ (∀ i ∉ s, lam i = 0) ∧ ∑ i ∈ s, lam i = 1 ∧ ∑ i ∈ s, lam i • a i = x ∧ z = ∑ i ∈ s, ↑(lam i) * ↑(alpha i)}

Text 5.6.1: Suppose f_i(x) = δ(x | a_i) + alpha_i, so f_i(x) = alpha_i when x = a_i and f_i(x) = +∞ otherwise. Let f be the convex hull of {f_i}. Then f is the greatest convex function with f(a_i) ≤ alpha_i for all i, and f(x) = inf { Σ_i lambda_i alpha_i | Σ_i lambda_i a_i = x }, where the infimum ranges over convex combinations with only finitely many nonzero coefficients.

theorem convexHullFunctionFamily_eq_sInf_convexCombination_univ {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (x : Fin n → ℝ) : convexHullFunctionFamily f x = sInf {z : EReal | ∃ (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) * f i (x' i)}

Specialize the convex-combination formula to Fin m by using Finset.univ.

theorem rightScalarMultiple_smul_eq {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {lam : Fin m → ℝ} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) {i : Fin m} {x : Fin n → ℝ} (hlam : 0 ≤ lam i) : rightScalarMultiple (f i) (lam i) (lam i • x) = ↑(lam i) * f i x

Right scalar multiple at a scaled point for a nonnegative coefficient.

theorem infimalConvolutionFamily_rightScalarMultiple_eq_sInf {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} {lam : Fin m → ℝ} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hlam : ∀ (i : Fin m), 0 ≤ lam i) (x : Fin n → ℝ) : infimalConvolutionFamily (fun (i : Fin m) => rightScalarMultiple (f i) (lam i)) x = sInf {z : EReal | ∃ (x' : Fin m → Fin n → ℝ), ∑ i : Fin m, lam i • x' i = x ∧ z = ∑ i : Fin m, ↑(lam i) * f i (x' i)}

Change of variables for infimal convolution of right scalar multiples.

theorem convexHullFunctionFamily_eq_sInf_infimalConvolution_rightScalarMultiple {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (x : Fin n → ℝ) : convexHullFunctionFamily f x = sInf {z : EReal | ∃ (lam : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ z = infimalConvolutionFamily (fun (i : Fin m) => rightScalarMultiple (f i) (lam i)) x}

Text 5.6.2: Assume I = {1, ..., m} and f_1, ..., f_m are proper convex functions. Let f = conv {f_1, ..., f_m}. Then f(x) = inf { (f_1 λ_1 □ ... □ f_m λ_m)(x) | λ_i ≥ 0, Σ_i λ_i = 1 }, where f_i λ_i denotes the right scalar multiple and □ is infimal convolution.