theorem section13_supportFunctionEReal_closedProperConvex_posHom {n : ℕ} (C : Set (Fin n → ℝ)) (hCne : C.Nonempty) (hC : Convex ℝ C) : ClosedConvexFunction (supportFunctionEReal C) ∧ ProperConvexFunctionOn Set.univ (supportFunctionEReal C) ∧ PositivelyHomogeneous (supportFunctionEReal C)

For a nonempty convex set C, its EReal-valued support function is closed, proper, convex, and positively homogeneous.

theorem section13_supportFunctionEReal_ne_bot {n : ℕ} (C : Set (Fin n → ℝ)) (hCne : C.Nonempty) (hC : Convex ℝ C) (xStar : Fin n → ℝ) : supportFunctionEReal C xStar ≠ ⊥

The EReal-valued support function of a nonempty convex set never takes the value ⊥.

theorem section13_supportFunctionEReal_subadditive {n : ℕ} (C : Set (Fin n → ℝ)) (hCne : C.Nonempty) (hC : Convex ℝ C) (xStar₁ xStar₂ : Fin n → ℝ) : supportFunctionEReal C (xStar₁ + xStar₂) ≤ supportFunctionEReal C xStar₁ + supportFunctionEReal C xStar₂

The EReal-valued support function of a nonempty convex set is subadditive.

theorem deltaStar_lowerSemicontinuous_and_add_le {n : ℕ} (C : Set (Fin n → ℝ)) (hCne : C.Nonempty) (hC : Convex ℝ C) : LowerSemicontinuous (supportFunctionEReal C) ∧ ∀ (xStar₁ xStar₂ : Fin n → ℝ), supportFunctionEReal C (xStar₁ + xStar₂) ≤ supportFunctionEReal C xStar₁ + supportFunctionEReal C xStar₂

Text 13.2.3: Let C ⊆ ℝ^n be a nonempty convex set. Then the (extended-real) support function is lower semicontinuous on ℝ^n, and it satisfies the subadditivity inequality

δ^*(xStar₁ + xStar₂ | C) ≤ δ^*(xStar₁ | C) + δ^*(xStar₂ | C) for all xStar₁, xStar₂.

theorem section13_sqrt_dotProduct_self_eq_norm_euclideanSpace {n : ℕ} (x : Fin n → ℝ) : √(x ⬝ᵥ x) = ‖(EuclideanSpace.equiv (Fin n) ℝ).symm x‖

Bridge Real.sqrt (dotProduct x x) to the Euclidean norm on EuclideanSpace.

theorem section13_dotProduct_le_sqrt_mul_sqrt {n : ℕ} (x y : Fin n → ℝ) : x ⬝ᵥ y ≤ √(x ⬝ᵥ x) * √(y ⬝ᵥ y)

Cauchy--Schwarz in the dotProduct notation used throughout this section.

theorem section13_dotProduct_le_sqrt_of_sqrt_dotProduct_self_le_one {n : ℕ} (x y : Fin n → ℝ) (hy : √(y ⬝ᵥ y) ≤ 1) : x ⬝ᵥ y ≤ √(x ⬝ᵥ x)

If y lies in the unit Euclidean ball, then dotProduct x y is bounded by the Euclidean norm of x.

theorem section13_exists_dotProduct_eq_sqrt {n : ℕ} (x : Fin n → ℝ) : ∃ (y : Fin n → ℝ), √(y ⬝ᵥ y) ≤ 1 ∧ x ⬝ᵥ y = √(x ⬝ᵥ x)

For any x, the supremum of y ↦ dotProduct x y over the unit Euclidean ball is attained by a normalized vector.

theorem euclideanNorm_eq_sSup_dotProduct_unitEuclideanBall_eq_deltaStar {n : ℕ} (x : Fin n → ℝ) : have B := {y : Fin n → ℝ | √(y ⬝ᵥ y) ≤ 1}; √(x ⬝ᵥ x) = sSup ((fun (y : Fin n → ℝ) => x ⬝ᵥ y) '' B) ∧ sSup ((fun (y : Fin n → ℝ) => x ⬝ᵥ y) '' B) = deltaStar B x

Text 13.2.4: Let B := { y ∈ ℝ^n | |y| ≤ 1 } be the unit Euclidean ball. Then for every x ∈ ℝ^n,

|x| = sup { ⟪x, y⟫ | y ∈ B } = δ^*(x | B).

theorem section13_mem_singleton_add_smul_unitEuclideanBall_iff {n : ℕ} (a z : Fin n → ℝ) (lam : ℝ) : have B := {y : Fin n → ℝ | √(y ⬝ᵥ y) ≤ 1}; z ∈ {a} + lam • B ↔ ∃ y ∈ B, z = a + lam • y

Membership in {a} + λ • B can be rewritten using the explicit parametrization a + λ • y, with y ∈ B.

theorem section13_dotProduct_le_dotProduct_add_mul_sqrt_of_mem_singleton_add_smul_unitEuclideanBall {n : ℕ} (a x z : Fin n → ℝ) (lam : ℝ) (hlam : 0 ≤ lam) : have B := {y : Fin n → ℝ | √(y ⬝ᵥ y) ≤ 1}; z ∈ {a} + lam • B → x ⬝ᵥ z ≤ x ⬝ᵥ a + lam * √(x ⬝ᵥ x)

Every dot product over the translated/scaled unit Euclidean ball is bounded by ⟪x, a⟫ + λ‖x‖ when λ ≥ 0.

theorem section13_exists_mem_singleton_add_smul_unitEuclideanBall_dotProduct_eq {n : ℕ} (a x : Fin n → ℝ) (lam : ℝ) : have B := {y : Fin n → ℝ | √(y ⬝ᵥ y) ≤ 1}; ∃ z ∈ {a} + lam • B, x ⬝ᵥ z = x ⬝ᵥ a + lam * √(x ⬝ᵥ x)

The supremum of z ↦ ⟪x, z⟫ over {a} + λ • B is attained at a + λ • y, where y maximizes ⟪x, ·⟫ over B.

theorem deltaStar_singleton_add_smul_unitEuclideanBall {n : ℕ} (a x : Fin n → ℝ) (lam : ℝ) (hlam : 0 ≤ lam) : have B := {y : Fin n → ℝ | √(y ⬝ᵥ y) ≤ 1}; deltaStar ({a} + lam • B) x = x ⬝ᵥ a + lam * √(x ⬝ᵥ x)

Text 13.2.5: Let B := { y ∈ ℝ^n | |y| ≤ 1 } be the unit Euclidean ball. More generally, for any a ∈ ℝ^n and λ ≥ 0, the support function of the ball a + λ B is given by

δ^*(x | a + λ B) = ⟪x, a⟫ + λ |x|.