theorem section13_exists_affineMap_le_indicatorFunction_gt_of_not_mem_closure {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) {x : Fin n → ℝ} (hx : x ∉ closure C) (μ : ℝ) : ∃ (h : (Fin n → ℝ) →ᵃ[ℝ] ℝ), (∀ (y : Fin n → ℝ), ↑(h y) ≤ indicatorFunction C y) ∧ ↑μ < ↑(h x)

If x ∉ closure C and C is a nonempty convex set, then for any real μ there exists an affine map bounded above by indicatorFunction C whose value at x exceeds μ.

theorem section13_fenchelConjugate_deltaStar_eq_clConv_indicatorFunction {n : ℕ} (C : Set (Fin n → ℝ)) (hCne : C.Nonempty) (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)) : (fenchelConjugate n fun (xStar : Fin n → ℝ) => ↑(deltaStar C xStar)) = clConv n (indicatorFunction C)

Under directional boundedness, the conjugate of the (Real-valued) support function is the closed convex envelope of the indicator function.

theorem section13_clConv_indicatorFunction_eq_indicatorFunction_closure {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) : clConv n (indicatorFunction C) = indicatorFunction (closure C)

For a nonempty convex set C, the closed convex envelope of indicatorFunction C is the indicator function of closure C.

theorem fenchelConjugate_deltaStar_eq_clConv_indicatorFunction_eq_indicatorFunction_closure {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCne : C.Nonempty) (hCbd : ∀ (xStar : Fin n → ℝ), BddAbove ((fun (x : Fin n → ℝ) => x ⬝ᵥ xStar) '' C)) : (fenchelConjugate n fun (xStar : Fin n → ℝ) => ↑(deltaStar C xStar)) = clConv n (indicatorFunction C) ∧ clConv n (indicatorFunction C) = indicatorFunction (closure C)

Text 13.1.5: Let C ⊆ ℝ^n be a convex set and let δ(· | C) be its indicator function. Then

(δ^*(· | C))^* = cl δ(· | C) = δ(· | cl C).

In this development, cl δ(·|C) is represented by clConv n (indicatorFunction C).

noncomputable def supportFunctionEReal {n : ℕ} (C : Set (Fin n → ℝ)) : (Fin n → ℝ) → EReal

Auxiliary definition: the EReal-valued support function xStar ↦ sup_{x ∈ C} ⟪x, xStar⟫.

Equations

• supportFunctionEReal C xStar = sSup {z : EReal | ∃ x ∈ C, z = ↑(x ⬝ᵥ xStar)}

theorem section13_fenchelConjugate_indicatorFunction_eq_supportFunctionEReal {n : ℕ} (C : Set (Fin n → ℝ)) : fenchelConjugate n (indicatorFunction C) = supportFunctionEReal C

Text 13.1.4 (EReal version): the Fenchel conjugate of an indicator function is the EReal-valued support function.

Auxiliary lemmas about scaling suprema in EReal.

theorem section13_mul_mul_inv_cancel_pos_real {a : ℝ} (ha : 0 < a) (z : EReal) : ↑a * (↑a⁻¹ * z) = z

For a > 0, multiplication by (a : EReal) cancels with multiplication by (a⁻¹ : EReal).

theorem section13_mul_inv_mul_cancel_pos_real {a : ℝ} (ha : 0 < a) (z : EReal) : ↑a⁻¹ * (↑a * z) = z

For a > 0, multiplication by (a⁻¹ : EReal) cancels with multiplication by (a : EReal).

theorem section13_ereal_mul_iSup_of_pos {ι : Sort u_1} (a : ℝ) (ha : 0 < a) (f : ι → EReal) : ↑a * iSup f = ⨆ (i : ι), ↑a * f i

Multiplying by (a : EReal) for a > 0 commutes with iSup.

theorem section13_fenchelConjugate_smul_eq_rightScalarMultiple {n : ℕ} (f : (Fin n → ℝ) → EReal) (lam : ℝ) (hlam : 0 < lam) : (fenchelConjugate n fun (x : Fin n → ℝ) => ↑lam * f x) = rightScalarMultiple (fenchelConjugate n f) lam

The Fenchel conjugate of a positive scalar multiple is the corresponding right scalar multiple of the Fenchel conjugate.

theorem section13_only_zero_top_iff_fenchelConjugate_posHom {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf_closed : ClosedConvexFunction f) (hf_proper : ProperConvexFunctionOn Set.univ f) : (∀ (x : Fin n → ℝ), f x = 0 ∨ f x = ⊤) ↔ PositivelyHomogeneous (fenchelConjugate n f)

A closed proper convex function is 0/⊤-valued iff its Fenchel conjugate is positively homogeneous.

theorem section13_eq_indicatorFunction_setOf_le_zero_of_only_zero_top {n : ℕ} (g : (Fin n → ℝ) → EReal) (hzeroTop : ∀ (x : Fin n → ℝ), g x = 0 ∨ g x = ⊤) : g = indicatorFunction {x : Fin n → ℝ | g x ≤ 0}

A 0/⊤-valued function with no ⊥ values is an indicator function of its 0-sublevel.

theorem indicatorFunction_conjugate_supportFunctionEReal_of_isClosed {n : ℕ} (C : Set (Fin n → ℝ)) (hC : Convex ℝ C) (hCclosed : IsClosed C) : fenchelConjugate n (indicatorFunction C) = supportFunctionEReal C ∧ fenchelConjugate n (supportFunctionEReal C) = indicatorFunction C

Theorem 13.2: The indicator function and the support function of a closed convex set are conjugate to each other. The functions which are the support functions of non-empty convex sets are the closed proper convex functions which are positively homogeneous.

theorem exists_supportFunctionEReal_iff_closedProperConvex_posHom {n : ℕ} (f : (Fin n → ℝ) → EReal) : (∃ (C : Set (Fin n → ℝ)), C.Nonempty ∧ Convex ℝ C ∧ f = supportFunctionEReal C) ↔ ClosedConvexFunction f ∧ ProperConvexFunctionOn Set.univ f ∧ PositivelyHomogeneous f

Theorem 13.2 (characterization of support functions): an EReal-valued function on ℝ^n is a support function of a nonempty convex set iff it is closed, proper, convex, and positively homogeneous.

theorem section13_setOf_forall_dotProduct_le_eq_setOf_fenchelConjugate_le_zero {n : ℕ} (f : (Fin n → ℝ) → EReal) : {xStar : Fin n → ℝ | ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ f x} = {xStar : Fin n → ℝ | fenchelConjugate n f xStar ≤ 0}

The set {xStar | ∀ x, ⟪x, xStar⟫ ≤ f x} is the 0-sublevel set of the Fenchel conjugate f*.

theorem section13_fenchelConjugate_eq_top_of_exists_dotProduct_gt {n : ℕ} (f : (Fin n → ℝ) → EReal) (hpos : PositivelyHomogeneous f) (xStar : Fin n → ℝ) (hx : ∃ (x : Fin n → ℝ), f x < ↑(x ⬝ᵥ xStar)) : fenchelConjugate n f xStar = ⊤

If there exists a strict supporting violation f x < ⟪x, xStar⟫, then f*(xStar) = ⊤.

theorem section13_fenchelConjugate_eq_zero_of_forall_dotProduct_le {n : ℕ} (f : (Fin n → ℝ) → EReal) (hpos : PositivelyHomogeneous f) (hnotTop : ¬∀ (x : Fin n → ℝ), f x = ⊤) (xStar : Fin n → ℝ) (hx : ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ f x) : fenchelConjugate n f xStar = 0

If all supporting inequalities ⟪x, xStar⟫ ≤ f x hold (and f is not identically ⊤), then f*(xStar) = 0.

theorem clConv_eq_supportFunctionEReal_setOf_forall_dotProduct_le {n : ℕ} (f : (Fin n → ℝ) → EReal) (hpos : PositivelyHomogeneous f) (_hconv : ConvexFunction f) (hnotTop : ¬∀ (x : Fin n → ℝ), f x = ⊤) : ∃ (C : Set (Fin n → ℝ)), IsClosed C ∧ Convex ℝ C ∧ clConv n f = supportFunctionEReal C ∧ C = {xStar : Fin n → ℝ | ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) ≤ f x}

Corollary 13.2.1. Let f be a positively homogeneous convex function which is not identically ⊤ (+∞). Then cl f (here represented by clConv n f) is the support function of the closed convex set

C = { xStar | ∀ x, ⟪x, xStar⟫ ≤ f x }.