theorem section13_dotProduct_head_succ {n : ℕ} (v w : Fin (n + 1) → ℝ) : v ⬝ᵥ w = v 0 * w 0 + (fun (i : Fin n) => v i.succ) ⬝ᵥ fun (i : Fin n) => w i.succ

Splitting a dot product in ℝ^{n+1} into its head and tail parts.

def section13_supportSet {n : ℕ} (f : (Fin n → ℝ) → EReal) : Set (Fin (n + 1) → ℝ)

The set C = { (λ^*, x^*) | λ^* ≤ -f^*(x^*) } ⊆ ℝ^{n+1} from Corollary 13.5.1.

theorem section13_supportFunctionEReal_supportSet_pos {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_proper : ProperConvexFunctionOn Set.univ f) (v : Fin (n + 1) → ℝ) (hpos : 0 < v 0) : supportFunctionEReal (section13_supportSet f) v = fenchelConjugate n (fun (xStar : Fin n → ℝ) => ↑(v 0) * fenchelConjugate n f xStar) fun (i : Fin n) => v i.succ

For λ > 0, the support function of section13_supportSet f at (λ,x) is the Fenchel conjugate of the scaled conjugate λ • f^*.

theorem section13_supportFunctionEReal_supportSet_pos_eq_rightScalarMultiple {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) (v : Fin (n + 1) → ℝ) (hpos : 0 < v 0) : supportFunctionEReal (section13_supportSet f) v = rightScalarMultiple f (v 0) fun (i : Fin n) => v i.succ

For λ > 0, supportFunctionEReal (section13_supportSet f) matches the rightScalarMultiple branch of Corollary 13.5.1.

theorem section13_supportFunctionEReal_supportSet_zero {n : ℕ} (f : (Fin n → ℝ) → EReal) (v : Fin (n + 1) → ℝ) (hzero : v 0 = 0) : supportFunctionEReal (section13_supportSet f) v = supportFunctionEReal (effectiveDomain Set.univ (fenchelConjugate n f)) fun (i : Fin n) => v i.succ

For λ = 0, the support function of section13_supportSet f reduces to the support function of dom f^*, evaluated at the tail vector.

theorem section13_supportFunctionEReal_supportSet_neg {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_proper : ProperConvexFunctionOn Set.univ f) (v : Fin (n + 1) → ℝ) (hneg : v 0 < 0) : supportFunctionEReal (section13_supportSet f) v = ⊤

For λ < 0, the support function of section13_supportSet f is ⊤.

theorem supportFunctionEReal_setOf_le_neg_fenchelConjugate_eq_piecewise_rightScalarMultiple {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : have k := fun (v : Fin (n + 1) → ℝ) => have lam := v 0; have x := fun (i : Fin n) => v i.succ; if _hpos : 0 < lam then rightScalarMultiple f lam x else if _hzero : lam = 0 then recessionFunction f x else ⊤; have C := {vStar : Fin (n + 1) → ℝ | ↑(vStar 0) ≤ -fenchelConjugate n f fun (i : Fin n) => vStar i.succ}; k = supportFunctionEReal C

Corollary 13.5.1. Let f be a closed proper convex function on ℝ^n. Define a function k : ℝ^{n+1} → (-∞, +∞] by

k(λ, x) = (f λ)(x) if λ > 0, k(0, x) = (f0^+)(x) if λ = 0, and k(λ, x) = +∞ if λ < 0.

Then k is the support function of the set C = { (λ^*, x^*) | λ^* ≤ -f^*(x^*) } ⊆ ℝ^{n+1}.

theorem section13_dotProduct_mulVec_right {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (x y : Fin n → ℝ) : x ⬝ᵥ A.mulVec y = A.transpose.mulVec x ⬝ᵥ y

Move mulVec from the right argument of dotProduct to the left.

theorem section13_deltaStar_image_mulVec {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (C : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) : deltaStar ((fun (y : Fin n → ℝ) => A.mulVec y) '' C) xStar = deltaStar C (A.transpose.mulVec xStar)

Support function under a linear image y ↦ A y: δ^*(x | A '' C) = δ^*(Aᵀ x | C).

theorem section13_deltaStar_singleton {n : ℕ} (a xStar : Fin n → ℝ) : deltaStar {a} xStar = xStar ⬝ᵥ a

The support function of a singleton is just the dot product.

theorem section13_posDef_dotProduct_mulVec_nonneg {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℝ} (hQ : Q.PosDef) (x : Fin n → ℝ) : 0 ≤ x ⬝ᵥ Q.mulVec x

Quadratic forms from positive definite matrices are nonnegative.

theorem section13_posDef_exists_isUnit_transpose_mul_self {n : ℕ} {Q : Matrix (Fin n) (Fin n) ℝ} (hQ : Q.PosDef) : ∃ (B : Matrix (Fin n) (Fin n) ℝ), IsUnit B ∧ Q = B.transpose * B

A real positive definite matrix factors as Bᵀ * B with B invertible.

theorem section13_ellipticSet_completeSquare_mem {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (a : Fin n → ℝ) (α : ℝ) (hQ : Q.PosDef) : have C := {x : Fin n → ℝ | 1 / 2 * x ⬝ᵥ Q.mulVec x + a ⬝ᵥ x + α ≤ 0}; have b := -Q⁻¹.mulVec a; have β := 1 / 2 * a ⬝ᵥ Q⁻¹.mulVec a - α; ∀ (x : Fin n → ℝ), x ∈ C ↔ 1 / 2 * (x - b) ⬝ᵥ Q.mulVec (x - b) ≤ β

Completing the square for the elliptic quadratic inequality.

theorem section13_beta_nonneg_of_nonempty {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (a : Fin n → ℝ) (α : ℝ) (hQ : Q.PosDef) : have C := {x : Fin n → ℝ | 1 / 2 * x ⬝ᵥ Q.mulVec x + a ⬝ᵥ x + α ≤ 0}; have β := 1 / 2 * a ⬝ᵥ Q⁻¹.mulVec a - α; C.Nonempty → 0 ≤ β

Nonemptiness of the elliptic set forces the radius parameter β to be nonnegative.

theorem section13_setOf_half_dotProduct_self_le_eq_smul_unitEuclideanBall {n : ℕ} (β : ℝ) (hβ : 0 ≤ β) : {z : Fin n → ℝ | 1 / 2 * z ⬝ᵥ z ≤ β} = √(2 * β) • {y : Fin n → ℝ | √(y ⬝ᵥ y) ≤ 1}

The set {z | (1/2) * ⟪z, z⟫ ≤ β} is a scaling of the unit Euclidean ball.

theorem section13_bddAbove_image_dotProduct_centeredSublevel_posDef {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (β : ℝ) (xStar : Fin n → ℝ) (hQ : Q.PosDef) (hβ : 0 ≤ β) : BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' {x : Fin n → ℝ | 1 / 2 * x ⬝ᵥ Q.mulVec x ≤ β})

Boundedness in direction xStar for the centered ellipsoid {x | (1/2) ⟪x, Qx⟫ ≤ β}.

theorem section13_deltaStar_centeredSublevel_posDef {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (β : ℝ) (xStar : Fin n → ℝ) (hQ : Q.PosDef) (hβ : 0 ≤ β) : deltaStar {x : Fin n → ℝ | 1 / 2 * x ⬝ᵥ Q.mulVec x ≤ β} xStar = √(2 * β * xStar ⬝ᵥ Q⁻¹.mulVec xStar)

Support function of the centered ellipsoid {x | (1/2) ⟪x, Qx⟫ ≤ β} for positive definite Q.

theorem deltaStar_ellipticSet_eq {n : ℕ} (Q : Matrix (Fin n) (Fin n) ℝ) (a : Fin n → ℝ) (α : ℝ) (xStar : Fin n → ℝ) (hQ : Q.PosDef) : have C := {x : Fin n → ℝ | 1 / 2 * x ⬝ᵥ Q.mulVec x + a ⬝ᵥ x + α ≤ 0}; have b := -Q⁻¹.mulVec a; have β := 1 / 2 * a ⬝ᵥ Q⁻¹.mulVec a - α; C.Nonempty → deltaStar C xStar = xStar ⬝ᵥ b + √(2 * β * xStar ⬝ᵥ Q⁻¹.mulVec xStar)

Text 13.5.2: For the “elliptic” convex set

C = {x | (1/2) ⟪x, Qx⟫ + ⟪a, x⟫ + α ≤ 0},

where Q is a positive definite symmetric matrix, one has (assuming C ≠ ∅)

δ^*(xStar | C) = ⟪b, xStar⟫ + (2β ⟪xStar, Q⁻¹ xStar⟫)^{1/2},

where b = -Q⁻¹ a and β = (1/2) ⟪a, Q⁻¹ a⟫ - α.