def simplexSet (m : ℕ) : Set (Fin m → ℝ)

The simplex of nonnegative weights summing to 1.

theorem convex_simplexSet {m : ℕ} : Convex ℝ (simplexSet m)

The simplex is convex.

def projXLinearMap {n m : ℕ} : (Fin (n + m) → ℝ) →ₗ[ℝ] Fin n → ℝ

Projection onto the x coordinates (first n) in Fin (n+m).

def projLamLinearMap {n m : ℕ} : (Fin (n + m) → ℝ) →ₗ[ℝ] Fin m → ℝ

Projection onto the λ coordinates (last m) in Fin (n+m).

def lamXLinearMap {n m : ℕ} (i : Fin m) : (Fin (n + m) → ℝ) →ₗ[ℝ] Fin (n + 1) → ℝ

Linear map selecting the ith λ coordinate and all x coordinates.

theorem convexFunctionOn_perspective_coord {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (i : Fin m) : ConvexFunctionOn Set.univ fun (x : Fin (n + m) → ℝ) => if 0 ≤ x (Fin.natAdd n i) then rightScalarMultiple (f i) (x (Fin.natAdd n i)) fun (k : Fin n) => x (Fin.castAdd m k) else ⊤

Perspective convexity after selecting the ith λ coordinate.

theorem convexFunctionOn_indicator_simplex_precomp {n m : ℕ} : ConvexFunctionOn Set.univ fun (x : Fin (n + m) → ℝ) => indicatorFunction (simplexSet m) (projLamLinearMap x)

Indicator of the simplex, precomposed with the λ projection, is convex.

theorem finset_sum_ne_bot {α : Type u_1} [DecidableEq α] (s : Finset α) (f : α → EReal) (h : ∀ a ∈ s, f a ≠ ⊥) : s.sum f ≠ ⊥

Non-⊥ is preserved by finite sums.

theorem convexFunctionOn_inf_sum_rightScalarMultiple_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 | ∃ (lam : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ z = ∑ i : Fin m, rightScalarMultiple (f i) (lam i) x}

Theorem 5.8.2: Let f_1, ..., f_m be proper convex functions on ℝ^n. Then the function g(x) = inf { (f_1 λ_1)(x) + ... + (f_m λ_m)(x) | λ_i ≥ 0, λ_1 + ... + λ_m = 1 } is convex.

theorem convexFunctionOn_gsup {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : ConvexFunctionOn Set.univ fun (x : Fin (n + m) → ℝ) => ⨆ (i : Fin m), if 0 ≤ x (Fin.natAdd n i) then rightScalarMultiple (f i) (x (Fin.natAdd n i)) fun (k : Fin n) => x (Fin.castAdd m k) else ⊤

The pointwise supremum of the perspective-coordinate functions is convex.

theorem gsup_ne_bot {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hm : 0 < m) (x : Fin (n + m) → ℝ) : (⨆ (i : Fin m), if 0 ≤ x (Fin.natAdd n i) then rightScalarMultiple (f i) (x (Fin.natAdd n i)) fun (k : Fin n) => x (Fin.castAdd m k) else ⊤) ≠ ⊥

The pointwise supremum of the perspective-coordinate functions is never ⊥ when m > 0.

theorem convexFunctionOn_gind_add_gsup {n m : ℕ} {f : Fin m → (Fin n → ℝ) → EReal} (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (hm : 0 < m) : ConvexFunctionOn Set.univ fun (x : Fin (n + m) → ℝ) => indicatorFunction (simplexSet m) (projLamLinearMap x) + ⨆ (i : Fin m), if 0 ≤ x (Fin.natAdd n i) then rightScalarMultiple (f i) (x (Fin.natAdd n i)) fun (k : Fin n) => x (Fin.castAdd m k) else ⊤

Adding the simplex indicator to the supremum perspective term is convex.

theorem convexFunctionOn_inf_iSup_rightScalarMultiple_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 | ∃ (lam : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ z = ⨆ (i : Fin m), rightScalarMultiple (f i) (lam i) x}

Theorem 5.8.3: Let f_1, ..., f_m be proper convex functions on ℝ^n. Then h(x) = inf { max { (f_1 λ_1)(x), ..., (f_m λ_m)(x) } | λ_i ≥ 0, λ_1 + ... + λ_m = 1 } is convex.

theorem lam_combo_in_simplex {m : ℕ} {lamx lamy : Fin m → ℝ} {t : ℝ} (hx : lamx ∈ simplexSet m) (hy : lamy ∈ simplexSet m) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (fun (i : Fin m) => (1 - t) * lamx i + t * lamy i) ∈ simplexSet m

Convex combinations preserve the simplex constraints.

theorem mul_f_strict_lt_convex_combo {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) {x y : Fin n → ℝ} {lamx lamy α β t : ℝ} (hx : rightScalarMultiple f lamx x < ↑α) (hy : rightScalarMultiple f lamy y < ↑β) (ht0 : 0 < t) (ht1 : t < 1) (hlamx : 0 ≤ lamx) (hlamy : 0 ≤ lamy) : rightScalarMultiple f ((1 - t) * lamx + t * lamy) ((1 - t) • x + t • y) < ↑(1 - t) * ↑α + ↑t * ↑β

Strict inequality for scaled values along convex combinations.

theorem convexFunctionOn_inf_iSup_weighted_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 | ∃ (lam : Fin m → ℝ) (x' : Fin m → Fin n → ℝ), (∀ (i : Fin m), 0 ≤ lam i) ∧ ∑ i : Fin m, lam i = 1 ∧ ∑ i : Fin m, x' i = x ∧ z = ⨆ (i : Fin m), rightScalarMultiple (f i) (lam i) (x' i)}

Theorem 5.8.4: Let f_1, ..., f_m be proper convex functions on ℝ^n. Then the function k defined by k(x) = inf { max { λ_1 f_1(x_1), ..., λ_m f_m(x_m) } } is convex, with the infimum taken over λ_i ≥ 0, ∑ λ_i = 1, and x_1 + ... + x_m = x.