theorem section13_dotProduct_le_sSup_coord_of_simplex {n : ℕ} (x xStar : Fin n → ℝ) (hx0 : ∀ (j : Fin n), 0 ≤ x j) (hsum : ∑ j : Fin n, x j = 1) : x ⬝ᵥ xStar ≤ sSup (Set.range fun (j : Fin n) => xStar j)

For a probability vector x (nonnegative with total mass 1), dotProduct x xStar is bounded above by the supremum of the coordinates of xStar.

theorem section13_exists_coord_eq_sSup {n : ℕ} (xStar : Fin n → ℝ) (hn : 0 < n) : ∃ (j0 : Fin n), xStar j0 = sSup (Set.range fun (j : Fin n) => xStar j)

On the finite type Fin n with 0 < n, the supremum of the coordinate range is achieved by some coordinate.

theorem section13_simplexVertex_mem_and_dotProduct {n : ℕ} (j0 : Fin n) (xStar : Fin n → ℝ) : (∀ (j : Fin n), 0 ≤ Pi.single j0 1 j) ∧ ∑ j : Fin n, Pi.single j0 1 j = 1 ∧ Pi.single j0 1 ⬝ᵥ xStar = xStar j0

A simplex vertex Pi.single j0 1 has nonnegative coordinates summing to 1, and its dot product with xStar is the j0-th coordinate.

theorem supportFunctionEReal_C1_eq_sSup_coord {n : ℕ} (xStar : Fin n → ℝ) : 0 < n → have C₁ := {x : Fin n → ℝ | (∀ (j : Fin n), 0 ≤ x j) ∧ ∑ j : Fin n, x j = 1}; supportFunctionEReal C₁ xStar = ↑(sSup (Set.range fun (j : Fin n) => xStar j))

Text 13.2.6: As further examples, the support functions of the sets

C₁ = {x = (ξ₁, …, ξₙ) | (∀ j, 0 ≤ ξⱼ) ∧ (ξ₁ + ⋯ + ξₙ = 1)},

C₂ = {x = (ξ₁, …, ξₙ) | |ξ₁| + ⋯ + |ξₙ| ≤ 1},

C₃ = {x = (ξ₁, ξ₂) | ξ₁ < 0 ∧ ξ₂ ≤ ξ₁⁻¹},

C₄ = {x = (ξ₁, ξ₂) | 2 ξ₁ + ξ₂² ≤ 0},

are given by the following formulas. (Here we use supportFunctionEReal so that ⊤ represents +∞.)

theorem section13_dotProduct_le_sSup_abs_coord_of_l1Ball {n : ℕ} (x xStar : Fin n → ℝ) (hn : 0 < n) (hx : ∑ j : Fin n, |x j| ≤ 1) : x ⬝ᵥ xStar ≤ sSup (Set.range fun (j : Fin n) => |xStar j|)

For x in the ℓ¹ unit ball, dotProduct x xStar is bounded above by the ℓ∞ norm of xStar, expressed as sSup (range fun j ↦ |xStar j|).

theorem section13_l1Ball_single_sign_mem {n : ℕ} (xStar : Fin n → ℝ) (j0 : Fin n) : ∑ j : Fin n, |Pi.single j0 (if 0 ≤ xStar j0 then 1 else -1) j| ≤ 1

The signed coordinate vector Pi.single j0 (±1) has ℓ¹ norm 1, hence lies in the ℓ¹ unit ball.

theorem section13_dotProduct_single_sign_eq_abs {n : ℕ} (xStar : Fin n → ℝ) (j0 : Fin n) : Pi.single j0 (if 0 ≤ xStar j0 then 1 else -1) ⬝ᵥ xStar = |xStar j0|

The dot product of the signed coordinate vector Pi.single j0 (±1) with xStar equals |xStar j0|.

theorem supportFunctionEReal_C2_eq_sSup_abs_coord {n : ℕ} (xStar : Fin n → ℝ) : 0 < n → have C₂ := {x : Fin n → ℝ | ∑ j : Fin n, |x j| ≤ 1}; supportFunctionEReal C₂ xStar = ↑(sSup (Set.range fun (j : Fin n) => |xStar j|))

Text 13.2.6 (support function of C₂): for the ℓ¹ unit ball C₂ = {x | ∑ j, |xⱼ| ≤ 1}, the support function is max_j |xStarⱼ|.

theorem section13_supportFunctionEReal_C3_eq_top_of_neg_coord (xStar : Fin 2 → ℝ) (hneg : xStar 0 < 0 ∨ xStar 1 < 0) : have C₃ := {x : Fin 2 → ℝ | x 0 < 0 ∧ x 1 ≤ (x 0)⁻¹}; supportFunctionEReal C₃ xStar = ⊤

If one coordinate of xStar is negative, then the support function of C₃ is ⊤.

theorem section13_dotProduct_le_supportBound_C3 (x xStar : Fin 2 → ℝ) (hx0 : x 0 < 0) (hx1 : x 1 ≤ (x 0)⁻¹) (hxStar0 : 0 ≤ xStar 0) (hxStar1 : 0 ≤ xStar 1) : x ⬝ᵥ xStar ≤ -2 * √(xStar 0 * xStar 1)

For x ∈ C₃ and xStar ≥ 0, the dot product is bounded above by -2 * sqrt (xStar 0 * xStar 1).

theorem section13_supportFunctionEReal_C3_eq_zero_of_nonneg_and_mul_eq_zero (xStar : Fin 2 → ℝ) (hxStar0 : 0 ≤ xStar 0) (hxStar1 : 0 ≤ xStar 1) (hprod : xStar 0 * xStar 1 = 0) : have C₃ := {x : Fin 2 → ℝ | x 0 < 0 ∧ x 1 ≤ (x 0)⁻¹}; supportFunctionEReal C₃ xStar = 0

If xStar ≥ 0 and xStar 0 * xStar 1 = 0, then the support function of C₃ is 0.

theorem section13_exists_C3_point_dotProduct_eq_supportBound (xStar : Fin 2 → ℝ) (hxStar0 : 0 < xStar 0) (hxStar1 : 0 < xStar 1) : ∃ (x : Fin 2 → ℝ), x 0 < 0 ∧ x 1 ≤ (x 0)⁻¹ ∧ x ⬝ᵥ xStar = -2 * √(xStar 0 * xStar 1)

When xStar 0, xStar 1 > 0, the bound -2 * sqrt (xStar 0 * xStar 1) is attained on C₃.

theorem supportFunctionEReal_C3_eq_piecewise (xStar : Fin 2 → ℝ) : have C₃ := {x : Fin 2 → ℝ | x 0 < 0 ∧ x 1 ≤ (x 0)⁻¹}; supportFunctionEReal C₃ xStar = if 0 ≤ xStar 0 ∧ 0 ≤ xStar 1 then ↑(-2 * √(xStar 0 * xStar 1)) else ⊤

Text 13.2.6 (support function of C₃): for C₃ = {x = (ξ₁, ξ₂) | ξ₁ < 0 ∧ ξ₂ ≤ ξ₁⁻¹}, one has δ^*(xStar | C₃) = -2 * sqrt (ξ₁^* ξ₂^*) if xStar ≥ 0, and +∞ otherwise.

theorem section13_neg_mul_sq_div_two_add_mul_le (a b t : ℝ) (ha : 0 < a) : -t ^ 2 / 2 * a + t * b ≤ b ^ 2 / (2 * a)

For 0 < a, the concave quadratic t ↦ (-(t^2)/2) * a + t * b is bounded above by b^2 / (2 * a).

theorem section13_dotProduct_le_supportBound_C4 (x xStar : Fin 2 → ℝ) (hxC4 : 2 * x 0 + x 1 ^ 2 ≤ 0) (hxStar0 : 0 < xStar 0) : x ⬝ᵥ xStar ≤ xStar 1 ^ 2 / (2 * xStar 0)

For x ∈ C₄ and 0 < xStar 0, the dot product is bounded above by (xStar 1)^2 / (2 * xStar 0).

theorem section13_exists_C4_point_dotProduct_eq_supportBound (xStar : Fin 2 → ℝ) (hxStar0 : 0 < xStar 0) : ∃ (x : Fin 2 → ℝ), 2 * x 0 + x 1 ^ 2 ≤ 0 ∧ x ⬝ᵥ xStar = xStar 1 ^ 2 / (2 * xStar 0)

For 0 < xStar 0, there exists a point of C₄ attaining the bound (xStar 1)^2 / (2 * xStar 0) in the dot product.

theorem section13_supportFunctionEReal_C4_eq_top_of_xStar0_lt_zero (xStar : Fin 2 → ℝ) (h0 : xStar 0 < 0) : have C₄ := {x : Fin 2 → ℝ | 2 * x 0 + x 1 ^ 2 ≤ 0}; supportFunctionEReal C₄ xStar = ⊤

If xStar 0 < 0, then the support function of C₄ is ⊤.

theorem section13_supportFunctionEReal_C4_eq_top_of_xStar0_eq_zero_and_xStar1_ne_zero (xStar : Fin 2 → ℝ) (h0 : xStar 0 = 0) (h1 : xStar 1 ≠ 0) : have C₄ := {x : Fin 2 → ℝ | 2 * x 0 + x 1 ^ 2 ≤ 0}; supportFunctionEReal C₄ xStar = ⊤

If xStar 0 = 0 and xStar 1 ≠ 0, then the support function of C₄ is ⊤.

theorem section13_supportFunctionEReal_C4_eq_zero_of_xStar_eq_zero (xStar : Fin 2 → ℝ) (h0 : xStar 0 = 0) (h1 : xStar 1 = 0) : have C₄ := {x : Fin 2 → ℝ | 2 * x 0 + x 1 ^ 2 ≤ 0}; supportFunctionEReal C₄ xStar = 0

If xStar = 0, then the support function of C₄ is 0.

theorem supportFunctionEReal_C4_eq_piecewise (xStar : Fin 2 → ℝ) : have C₄ := {x : Fin 2 → ℝ | 2 * x 0 + x 1 ^ 2 ≤ 0}; supportFunctionEReal C₄ xStar = if xStar 0 > 0 then ↑(xStar 1 ^ 2 / (2 * xStar 0)) else if xStar 0 = 0 ∧ xStar 1 = 0 then 0 else ⊤

Text 13.2.6 (support function of C₄): for C₄ = {x = (ξ₁, ξ₂) | 2 ξ₁ + ξ₂² ≤ 0}, one has δ^*(xStar | C₄) = (ξ₂^*)² / (2 * ξ₁^*) if ξ₁^* > 0, 0 if xStar = 0, and +∞ otherwise.

theorem section13_supportFunctionEReal_effectiveDomain_le_coe_iff {n : ℕ} (f : (Fin n → ℝ) → EReal) (y : Fin n → ℝ) (μ : ℝ) : supportFunctionEReal (effectiveDomain Set.univ f) y ≤ ↑μ ↔ ∀ x ∈ effectiveDomain Set.univ f, x ⬝ᵥ y ≤ μ

For the EReal-valued support function, an upper bound by a real μ is equivalent to a pointwise upper bound on all dot products defining the supremum.

theorem section13_recessionSup_le_coe_iff {n : ℕ} (g g0_plus : (Fin n → ℝ) → EReal) (hg0_plus : ∀ (y : Fin n → ℝ), g0_plus y = sSup {r : EReal | ∃ x ∈ effectiveDomain Set.univ g, r = g (x + y) - g x}) (y : Fin n → ℝ) (μ : ℝ) : g0_plus y ≤ ↑μ ↔ ∀ x ∈ effectiveDomain Set.univ g, g (x + y) - g x ≤ ↑μ

For the sSup-of-differences recession formula, bounding by a real μ is equivalent to a uniform pointwise bound on each difference term.

theorem section13_dotProduct_nsmul_right {n : ℕ} (x y : Fin n → ℝ) (m : ℕ) : x ⬝ᵥ m • y = ↑m * x ⬝ᵥ y

The dot product is additive in the second argument, hence it commutes with nsmul there.

theorem section13_fenchelConjugate_add_le_add_supportFunctionEReal {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) {y : Fin n → ℝ} {μ : ℝ} (hxy : ∀ x ∈ effectiveDomain Set.univ f, x ⬝ᵥ y ≤ μ) (xStar : Fin n → ℝ) : xStar ∈ effectiveDomain Set.univ (fenchelConjugate n f) → fenchelConjugate n f (xStar + y) - fenchelConjugate n f xStar ≤ ↑μ

If all dot products ⟪x,y⟫ over x ∈ dom f are bounded by μ, then every difference f*(xStar+y) - f*(xStar) with xStar ∈ dom f* is bounded by μ.

theorem supportFunctionEReal_effectiveDomain_eq_recession_fenchelConjugate {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) (fStar0_plus : (Fin n → ℝ) → EReal) (hfStar0_plus : ∀ (y : Fin n → ℝ), fStar0_plus y = sSup {r : EReal | ∃ xStar ∈ effectiveDomain Set.univ (fenchelConjugate n f), r = fenchelConjugate n f (xStar + y) - fenchelConjugate n f xStar}) : supportFunctionEReal (effectiveDomain Set.univ f) = fStar0_plus

Theorem 13.3: Let f be a proper convex function. The support function of dom f is the recession function (f^*)0+ of the conjugate f^*. If f is closed, the support function of dom f^* is the recession function f0+ of f.

theorem supportFunctionEReal_effectiveDomain_fenchelConjugate_eq_recession {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) (hclosed : ClosedConvexFunction f) (f0_plus : (Fin n → ℝ) → EReal) (hf0_plus : ∀ (y : Fin n → ℝ), f0_plus y = sSup {r : EReal | ∃ x ∈ effectiveDomain Set.univ f, r = f (x + y) - f x}) : supportFunctionEReal (effectiveDomain Set.univ (fenchelConjugate n f)) = f0_plus

Theorem 13.3 (closed case): if f is closed, then the support function of dom f^* is the recession function f0+ of f.