theorem section13_zero_mem_intrinsicInterior_iff_supportFunctionEReal {n : ℕ} (C : Set (Fin n → ℝ)) (hCconv : Convex ℝ C) (hCne : C.Nonempty) : 0 ∈ intrinsicInterior ℝ C ↔ ∀ (y : Fin n → ℝ), ¬(-supportFunctionEReal C (-y) = supportFunctionEReal C y ∧ supportFunctionEReal C y = 0) → supportFunctionEReal C y > 0

Support-function characterization of (0 : ℝ^n) ∈ ri C for convex nonempty C.

theorem section13_zero_mem_affineSpan_iff_supportFunctionEReal {n : ℕ} (C : Set (Fin n → ℝ)) (hCne : C.Nonempty) : 0 ∈ ↑(affineSpan ℝ C) ↔ ∀ (y : Fin n → ℝ), -supportFunctionEReal C (-y) = supportFunctionEReal C y → supportFunctionEReal C y = 0

Support-function characterization of 0 ∈ affineSpan C.

theorem mem_closure_ri_interior_affineSpan_effectiveDomain_fenchelConjugate_iff_recessionFunction {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) (xStar : Fin n → ℝ) : have domFstar := effectiveDomain Set.univ (fenchelConjugate n f); have g := fun (x : Fin n → ℝ) => f x - ↑(x ⬝ᵥ xStar); (xStar ∈ closure domFstar ↔ ∀ (y : Fin n → ℝ), 0 ≤ recessionFunction g y) ∧ (xStar ∈ intrinsicInterior ℝ domFstar ↔ ∀ (y : Fin n → ℝ), ¬(-recessionFunction g (-y) = recessionFunction g y ∧ recessionFunction g y = 0) → recessionFunction g y > 0) ∧ (xStar ∈ interior domFstar ↔ ∀ (y : Fin n → ℝ), y ≠ 0 → recessionFunction g y > 0) ∧ (xStar ∈ ↑(affineSpan ℝ domFstar) ↔ ∀ (y : Fin n → ℝ), -recessionFunction g (-y) = recessionFunction g y → recessionFunction g y = 0)

Corollary 13.3.4. Let f be a closed proper convex function. Let xStar be a fixed vector and let g x = f x - ⟪x, xStar⟫. Then:

(a) xStar ∈ cl (dom f^*) if and only if (g₀⁺) y ≥ 0 for every y; (b) xStar ∈ ri (dom f^*) if and only if (g₀⁺) y > 0 for all y except those satisfying -(g₀⁺ (-y)) = (g₀⁺) y = 0; (c) xStar ∈ int (dom f^*) if and only if (g₀⁺) y > 0 for every y ≠ 0; (d) xStar ∈ aff (dom f^*) if and only if (g₀⁺) y = 0 for every y such that -(g₀⁺ (-y)) = (g₀⁺) y.

Here f^* is fenchelConjugate n f, its domain is effectiveDomain univ (fenchelConjugate n f), and g₀⁺ is recessionFunction g.

theorem section13_linearitySpace_fenchelConjugate_iff_supportFunctionEReal_effectiveDomain {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) (y : Fin n → ℝ) : y ∈ linearitySpace (fenchelConjugate n f) ↔ supportFunctionEReal (effectiveDomain Set.univ f) y ≠ ⊤ ∧ -supportFunctionEReal (effectiveDomain Set.univ f) (-y) = supportFunctionEReal (effectiveDomain Set.univ f) y

Rewrite linearitySpace (f*) using Theorem 13.3: it is a finiteness+symmetry condition on the support function of dom f.

theorem section13_supportFunctionEReal_symm_finite_imp_dotProduct_const {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) {y : Fin n → ℝ} (hy : supportFunctionEReal C y ≠ ⊤) (hsymm : -supportFunctionEReal C (-y) = supportFunctionEReal C y) : ∃ (μ : ℝ), ∀ x ∈ C, x ⬝ᵥ y = μ

If a support function is finite and symmetric at y, then the dot-product functional x ↦ ⟪x,y⟫ is constant on the underlying set.

theorem section13_dotProduct_const_iff_mem_orthogonalComplement_direction_affineSpan {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) (y : Fin n → ℝ) : (∃ (μ : ℝ), ∀ x ∈ C, x ⬝ᵥ y = μ) ↔ y ∈ orthogonalComplement n (affineSpan ℝ C).direction

The dot-product functional x ↦ ⟪x,y⟫ is constant on a nonempty set C iff y is orthogonal to the direction of affineSpan C.

theorem section13_finrank_orthogonalComplement {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) : Module.finrank ℝ ↥(orthogonalComplement n L) = n - Module.finrank ℝ ↥L

Finite-dimensional formula: dim(Lᗮ) = n - dim(L) for the book’s orthogonalComplement.