theorem section13_finrank_direction_affineSpan_effectiveDomain_le {n : ℕ} (f : (Fin n → ℝ) → EReal) : Module.finrank ℝ ↥(affineSpan ℝ (effectiveDomain Set.univ f)).direction ≤ n

For any f : ℝ^n → (-∞, +∞], the direction of affineSpan (dom f) has finrank at most n.

theorem section13_rank_eq_rank_fenchelConjugate {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : have rank := fun (h : (Fin n → ℝ) → EReal) => Module.finrank ℝ ↥(affineSpan ℝ (effectiveDomain Set.univ h)).direction - Module.finrank ℝ ↥(Submodule.span ℝ (linearitySpace h)); rank (fenchelConjugate n f) = rank f

The book-defined rank dim(aff(dom f)) - lin(f) is invariant under Fenchel conjugation.

theorem rank_eq_of_conjugate {n : ℕ} {f g : (Fin n → ℝ) → EReal} (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) (hg_closed : ClosedConvexFunction g) (hg_proper : ProperConvexFunctionOn Set.univ g) (hfg : fenchelConjugate n f = g) (hgf : fenchelConjugate n g = f) : have rank := fun (h : (Fin n → ℝ) → EReal) => Module.finrank ℝ ↥(affineSpan ℝ (effectiveDomain Set.univ h)).direction - Module.finrank ℝ ↥(Submodule.span ℝ (linearitySpace h)); rank f = rank g

Corollary 13.4.1. Closed proper convex functions conjugate to each other have the same rank.

def section13_dotProductHyperplane {n : ℕ} (y : Fin n → ℝ) (a : ℝ) : AffineSubspace ℝ (Fin n → ℝ)

The affine hyperplane {x | ⟪y, x⟫ = a} as an AffineSubspace.

Equations

• section13_dotProductHyperplane y a = { carrier := {xStar : Fin n → ℝ | y ⬝ᵥ xStar = a}, smul_vsub_vadd_mem := ⋯ }

theorem section13_fenchelConjugate_eq_top_of_affineLine {n : ℕ} (f : (Fin n → ℝ) → EReal) {x y xStar : Fin n → ℝ} {a b : ℝ} (hline : ∀ (t : ℝ), f (x + t • y) = ↑(a * t + b)) (hcoeff : y ⬝ᵥ xStar ≠ a) : fenchelConjugate n f xStar = ⊤

If f is affine along a line, then its Fenchel conjugate is ⊤ off the corresponding hyperplane in the dual variable.

theorem section13_not_nonempty_interior_dom_fenchelConjugate_of_exists_affineLine {n : ℕ} (f : (Fin n → ℝ) → EReal) (hline : ∃ (x : Fin n → ℝ) (y : Fin n → ℝ), y ≠ 0 ∧ ∃ (a : ℝ) (b : ℝ), ∀ (t : ℝ), f (x + t • y) = ↑(a * t + b)) : ¬(interior (effectiveDomain Set.univ (fenchelConjugate n f))).Nonempty

If f is affine along a line with direction y ≠ 0, then dom (f*) has empty interior.

def section13_addRightOrderIso (c : ℝ) : EReal ≃o EReal

Addition by a real constant as an order isomorphism on EReal.

Equations

• section13_addRightOrderIso c = { toFun := fun (x : EReal) => x + ↑c, invFun := fun (x : EReal) => x - ↑c, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem section13_sSup_image_add_right (c : ℝ) (s : Set EReal) : sSup ((fun (z : EReal) => z + ↑c) '' s) = sSup s + ↑c

sSup commutes with addition by a real constant on EReal.

theorem section13_fenchelConjugate_translate_of_dotProduct_const {n : ℕ} (g : (Fin n → ℝ) → EReal) (hg_bot : ∀ (xStar : Fin n → ℝ), g xStar ≠ ⊥) {y : Fin n → ℝ} {μ : ℝ} (hμ : ∀ xStar ∈ effectiveDomain Set.univ g, xStar ⬝ᵥ y = μ) (x : Fin n → ℝ) (t : ℝ) : fenchelConjugate n g (x + t • y) = fenchelConjugate n g x + ↑(t * μ)

If the dot product xStar ↦ ⟪xStar, y⟫ is constant on dom g, then fenchelConjugate n g is affine along the line x + t • y.

theorem section13_orthogonalComplement_eq_top_iff {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) : orthogonalComplement n L = ⊤ ↔ L = ⊥

For the book’s orthogonalComplement, one has Lᗮ = ⊤ iff L = ⊥.

theorem section13_orthogonalComplement_orthogonalComplement_eq {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) : orthogonalComplement n (orthogonalComplement n L) = L

In finite dimension, the book orthogonal complement is involutive: (Lᗮ)ᗮ = L.

theorem section13_exists_nonzero_mem_linearitySpace_of_not_nonempty_interior_dom_fenchelConjugate {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) (hno : ¬(interior (effectiveDomain Set.univ (fenchelConjugate n f))).Nonempty) : ∃ (y : Fin n → ℝ), y ≠ 0 ∧ y ∈ linearitySpace f

If dom (f*) has empty interior, then linearitySpace f contains a nonzero direction.

theorem section13_exists_affineLine_of_mem_linearitySpace {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) {y : Fin n → ℝ} (hy0 : y ≠ 0) (hy : y ∈ linearitySpace f) : ∃ (x : Fin n → ℝ) (y : Fin n → ℝ), y ≠ 0 ∧ ∃ (a : ℝ) (b : ℝ), ∀ (t : ℝ), f (x + t • y) = ↑(a * t + b)

A nonzero direction in linearitySpace f yields an affine line along which f is finite and affine.

theorem effectiveDomain_fenchelConjugate_interior_nonempty_iff_not_exists_affineLine {n : ℕ} (f : (Fin n → ℝ) → EReal) (hclosed : ClosedConvexFunction f) (hproper : ProperConvexFunctionOn Set.univ f) : (interior (effectiveDomain Set.univ (fenchelConjugate n f))).Nonempty ↔ ¬∃ (x : Fin n → ℝ) (y : Fin n → ℝ), y ≠ 0 ∧ ∃ (a : ℝ) (b : ℝ), ∀ (t : ℝ), f (x + t • y) = ↑(a * t + b)

Corollary 13.4.2. Let f be a closed proper convex function. Then dom f^* has a non-empty interior if and only if there are no lines along which f is (finite and) affine.

Here f^* is the Fenchel conjugate fenchelConjugate n f, and dom f^* is its effective domain effectiveDomain univ (fenchelConjugate n f). The absence of a line along which f is finite and affine is expressed by the nonexistence of x and a nonzero direction y such that t ↦ f (x + t • y) agrees with an affine function of t.

theorem section13_levelSet_eq_setOf_sub_dotProduct_sub_le_zero {n : ℕ} (h : (Fin n → ℝ) → EReal) (bStar : Fin n → ℝ) (β : ℝ) : {x : Fin n → ℝ | h x ≤ ↑β + ↑(x ⬝ᵥ bStar)} = {x : Fin n → ℝ | h x - ↑(x ⬝ᵥ bStar) - ↑β ≤ 0}

Rewriting a dot-product level set as a ≤ 0 sublevel set by moving affine terms across the inequality in EReal.

theorem section13_fenchelConjugate_sub_const {n : ℕ} (g : (Fin n → ℝ) → EReal) (β : ℝ) : (fenchelConjugate n fun (x : Fin n → ℝ) => g x - ↑β) = fun (xStar : Fin n → ℝ) => fenchelConjugate n g xStar + ↑β

Subtracting a real constant from the primal function adds that constant to its Fenchel conjugate.

theorem levelSet_le_add_dotProduct_eq_setOf_sub_dotProduct_sub_le_zero_and_fenchelConjugate {n : ℕ} (h : (Fin n → ℝ) → EReal) (bStar : Fin n → ℝ) (β : ℝ) : have C := {x : Fin n → ℝ | h x ≤ ↑β + ↑(x ⬝ᵥ bStar)}; have f := fun (x : Fin n → ℝ) => h x - ↑(x ⬝ᵥ bStar) - ↑β; C = {x : Fin n → ℝ | f x ≤ 0} ∧ ∀ (xStar : Fin n → ℝ), fenchelConjugate n f xStar = fenchelConjugate n h (xStar + bStar) + ↑β

Text 13.4.3: Let h : ℝ^n → (-∞, +∞] be a proper convex function, let bStar ∈ ℝ^n, and let β ∈ ℝ. Define the level set C := {x | h x ≤ β + ⟪x, bStar⟫} and the shifted function f x := h x - ⟪x, bStar⟫ - β. Then C = {x | f x ≤ 0}. Moreover, the Fenchel conjugate of f satisfies f^*(xStar) = h^*(xStar + bStar) + β for all xStar ∈ ℝ^n.

theorem section13_posHom_dotProduct {n : ℕ} (xStar : Fin n → ℝ) : PositivelyHomogeneous fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar)

The linear functional x ↦ ⟪x, xStar⟫ is positively homogeneous when viewed as an EReal-valued function.

theorem section13_convexFunctionOn_dotProduct {n : ℕ} (xStar : Fin n → ℝ) : ConvexFunctionOn Set.univ fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar)

The linear functional x ↦ ⟪x, xStar⟫ is convex on ℝ^n (its epigraph is a half-space).

theorem section13_setOf_forall_dotProduct_le_posHomGenerated_eq {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : ConvexFunctionOn Set.univ f) : have k := positivelyHomogeneousConvexFunctionGenerated f; {xStar : Fin n → ℝ | ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ k x} = {xStar : Fin n → ℝ | ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ f x}

Majorants of the positively homogeneous hull coincide with majorants of the original convex function.

theorem section13_clConv_posHomGenerated_eq_supportFunctionEReal_setOf_fenchelConjugate_le_zero {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : clConv n (positivelyHomogeneousConvexFunctionGenerated f) = supportFunctionEReal {xStar : Fin n → ℝ | fenchelConjugate n f xStar ≤ 0}

The closed positively homogeneous hull of a closed proper convex function f is the support function of the polar set {xStar | f*(xStar) ≤ 0}.

theorem section13_supportFunctionEReal_setOf_le_zero_eq_clConv_posHomGenerated_fenchelConjugate {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : supportFunctionEReal {x : Fin n → ℝ | f x ≤ 0} = clConv n (positivelyHomogeneousConvexFunctionGenerated (fenchelConjugate n f))

The support function of the 0-sublevel set of f is the closed positively homogeneous hull of f*.

theorem supportFunctionEReal_setOf_le_zero_eq_clConv_posHomGenerated_fenchelConjugate_and_dual {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : supportFunctionEReal {x : Fin n → ℝ | f x ≤ 0} = clConv n (positivelyHomogeneousConvexFunctionGenerated (fenchelConjugate n f)) ∧ clConv n (positivelyHomogeneousConvexFunctionGenerated f) = supportFunctionEReal {xStar : Fin n → ℝ | fenchelConjugate n f xStar ≤ 0}

Theorem 13.5. Let f be a closed proper convex function. The support function of { x | f x ≤ 0 } is cl g, where g is the positively homogeneous convex function generated by f*. Dually, the closure of the positively homogeneous convex function k generated by f is the support function of { xStar | f*(xStar) ≤ 0 }.

Here f* is the Fenchel conjugate fenchelConjugate n f; the support function is represented by supportFunctionEReal; the closure cl is represented by clConv n; and the positively homogeneous convex function generated by a function h is positivelyHomogeneousConvexFunctionGenerated h.