def CoFiniteConvexFunction {n : ℕ} (f : (Fin n → ℝ) → EReal) : Prop

Text 13.3.1: A convex function f is called co-finite if f is closed and proper and epi f contains no non-vertical half-lines; equivalently, its recession function f₀⁺ satisfies f₀⁺(y) = +∞ for all y ≠ 0.

theorem section13_effectiveDomain_nonempty_of_proper {n : ℕ} {f : (Fin n → ℝ) → EReal} : ProperConvexFunctionOn Set.univ f → (effectiveDomain Set.univ f).Nonempty

If f is proper on univ, then its effective domain is nonempty.

theorem section13_exists_mem_add_not_mem_effectiveDomain_of_isBounded {n : ℕ} {D : Set (Fin n → ℝ)} (hbounded : Bornology.IsBounded D) (hne : D.Nonempty) {y : Fin n → ℝ} (hy : y ≠ 0) : ∃ x ∈ D, x + y ∉ D

A bounded set cannot contain all iterates x + n • y for a nonzero vector y.

theorem section13_sSup_recession_eq_top_of_exists_not_mem {n : ℕ} {f : (Fin n → ℝ) → EReal} {y : Fin n → ℝ} : (∃ x ∈ effectiveDomain Set.univ f, x + y ∉ effectiveDomain Set.univ f) → sSup {r : EReal | ∃ x ∈ effectiveDomain Set.univ f, r = f (x + y) - f x} = ⊤

If x ∈ dom f but x+y ∉ dom f, then the recession sSup in direction y is ⊤.

theorem coFiniteConvexFunction_of_isBounded_effectiveDomain {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) (hbounded : Bornology.IsBounded (effectiveDomain Set.univ f)) : CoFiniteConvexFunction f

Text 13.3.2: Let f : ℝ^n → (-∞, +∞] be closed, proper, and convex. If dom f is bounded, then f is co-finite.

theorem section13_supportFunctionEReal_univ_eq_top_of_ne_zero {n : ℕ} {y : Fin n → ℝ} (hy : y ≠ 0) : supportFunctionEReal Set.univ y = ⊤

The support function of Set.univ is ⊤ in any nonzero direction.

theorem section13_proper_of_conjugate_finite_everywhere {n : ℕ} {f : (Fin n → ℝ) → EReal} (hclosed : ClosedConvexFunction f) (hfiniteStar : effectiveDomain Set.univ (fenchelConjugate n f) = Set.univ ∧ ∀ (xStar : Fin n → ℝ), fenchelConjugate n f xStar ≠ ⊥) : ProperConvexFunctionOn Set.univ f

If f* is finite everywhere (no ⊥ and dom f* = univ), then f is proper.

theorem effectiveDomain_fenchelConjugate_eq_univ_iff_coFinite {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) : (effectiveDomain Set.univ (fenchelConjugate n f) = Set.univ ∧ ∀ (xStar : Fin n → ℝ), fenchelConjugate n f xStar ≠ ⊥) ↔ CoFiniteConvexFunction f

Corollary 13.3.1. Let f be a closed convex function on ℝ^n. Then f^* is finite everywhere (equivalently dom f^* = ℝ^n) if and only if f is co-finite.

noncomputable def recessionFunction {n : ℕ} (f : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Auxiliary definition: the recession function f₀⁺ of an EReal-valued function f on ℝ^n, given by f₀⁺(y) = sup { f(x+y) - f(x) | x ∈ dom f }.

theorem section13_supportFunctionEReal_le_coe_iff {n : ℕ} (C : Set (Fin n → ℝ)) (y : Fin n → ℝ) (μ : ℝ) : supportFunctionEReal C y ≤ ↑μ ↔ ∀ x ∈ C, 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_supportFunctionEReal_coe_toReal {n : ℕ} {C : Set (Fin n → ℝ)} (hCne : C.Nonempty) {y : Fin n → ℝ} (hy : supportFunctionEReal C y ≠ ⊤) : ↑(supportFunctionEReal C y).toReal = supportFunctionEReal C y

If C is nonempty and supportFunctionEReal C y ≠ ⊤, then supportFunctionEReal C y is the coercion of its toReal.

theorem section13_supportFunctionEReal_affineSubspace_symmetry {n : ℕ} (A : AffineSubspace ℝ (Fin n → ℝ)) (hAne : (↑A).Nonempty) {y : Fin n → ℝ} (hy : supportFunctionEReal (↑A) y ≠ ⊤) : -supportFunctionEReal (↑A) (-y) = supportFunctionEReal (↑A) y

On an affine subspace, if the support function is finite at y, then it is symmetric.

theorem section13_isAffineSet_iff_supportFunction_symmetry {n : ℕ} {C : Set (Fin n → ℝ)} (hCconv : Convex ℝ C) (hCne : C.Nonempty) : (∃ (A : AffineSubspace ℝ (Fin n → ℝ)), ↑A = C) ↔ ∀ (y : Fin n → ℝ), supportFunctionEReal C y ≠ ⊤ → -supportFunctionEReal C (-y) = supportFunctionEReal C y

A convex set is affine iff its EReal support function is symmetric on the directions where it is finite.

theorem section13_supportFunctionEReal_dom_fenchelConjugate_eq_recessionFunction {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) : supportFunctionEReal (effectiveDomain Set.univ (fenchelConjugate n f)) = recessionFunction f

The support function of dom f* is the recession function recessionFunction f.

def linearitySpace {n : ℕ} (f : (Fin n → ℝ) → EReal) : Set (Fin n → ℝ)

Auxiliary definition: the linearity space of a function f, defined as the set of directions y for which the recession function is finite and symmetric: -(f₀⁺)(-y) = (f₀⁺)(y) whenever (f₀⁺)(y) < +∞.

theorem effectiveDomain_fenchelConjugate_isAffine_iff_forall_recessionFunction_eq_top_of_not_mem {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) : (∃ (A : AffineSubspace ℝ (Fin n → ℝ)), ↑A = effectiveDomain Set.univ (fenchelConjugate n f)) ↔ ∀ y ∉ linearitySpace f, recessionFunction f y = ⊤

Corollary 13.3.2. Let f be a closed proper convex function. In order that dom f* be an affine set, it is necessary and sufficient that (f0+)(y) = +∞ for every y which is not actually in the linearity space of f.