theorem section16_fenchelConjugate_sum_mul_log_eq_log_sum_exp {n : ℕ} (hn : 0 < n) : have f := fun (ξ : Fin n → ℝ) => if 0 ≤ ξ ∧ ∑ j : Fin n, ξ j = 1 then ↑(∑ j : Fin n, ξ j * Real.log (ξ j)) else ⊤; fenchelConjugate n f = fun (xStar : Fin n → ℝ) => ↑(Real.log (∑ j : Fin n, Real.exp (xStar j)))

Text 16.4.4: Let f : ℝⁿ → ℝ ∪ {+∞} be defined by

f(ξ₁, …, ξₙ) = ξ₁ log ξ₁ + ⋯ + ξₙ log ξₙ if ξⱼ ≥ 0 for all j and ∑ᵢ ξᵢ = 1, and f = +∞ otherwise (with the convention 0 log 0 = 0).

Then the Fenchel conjugate satisfies f^*(x^*) = log (exp(λ₁^*) + ⋯ + exp(λₙ^*)).

theorem section16_convexFunctionOn_dotProduct_sub_const {n : ℕ} (b : Fin n → ℝ) (μ : ℝ) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ b - μ)

The affine functional x ↦ ⟪x,b⟫ - μ is convex as an EReal-valued function.

theorem section16_affine_le_convexHullFunctionFamily_iff_forall_le {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) (b : Fin n → ℝ) (μ : ℝ) : (∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ b - μ) ≤ convexHullFunctionFamily f x) ↔ ∀ (i : ι) (x : Fin n → ℝ), ↑(x ⬝ᵥ b - μ) ≤ f i x

Affine minorants of the convex hull coincide with affine minorants of each family member.

theorem section16_fenchelConjugate_convexHullFunctionFamily_le_coe_iff_forall {n : ℕ} {ι : Sort u_1} (f : ι → (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) (μ : ℝ) : fenchelConjugate n (convexHullFunctionFamily f) xStar ≤ ↑μ ↔ ∀ (i : ι), fenchelConjugate n (f i) xStar ≤ ↑μ

The epigraph inequality for the convex hull reduces to the family componentwise.

theorem section16_sSup_range_fenchelConjugate_ne_bot_of_nonempty {n : ℕ} {ι : Sort u_1} [Nonempty ι] (f : ι → (Fin n → ℝ) → EReal) (hf : ∀ (i : ι), ProperConvexFunctionOn Set.univ (f i)) (xStar : Fin n → ℝ) : sSup (Set.range fun (i : ι) => fenchelConjugate n (f i) xStar) ≠ ⊥

Nonempty families yield a non-⊥ supremum of conjugates.

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

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

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

Here conv {f_i | i ∈ I} is represented by convexHullFunctionFamily f, and f_i^* is fenchelConjugate n (f i).