theorem convexFunctionOn_inf_iSup_of_proper {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => sInf {z : EReal | ∃ (x' : Fin m → Fin n → ℝ), ∑ i : Fin m, x' i = x ∧ z = ⨆ (i : Fin m), f i (x' i)}

Theorem 5.8.1: Let f_1, ..., f_m be proper convex functions on ℝ^n. Then f(x) = inf { max { f_1(x_1), ..., f_m(x_m) } | x_1 + ... + x_m = x } is convex.