theorem fenchelConjugate_symm_bijOn_closedProperConvex (n : ℕ) : Set.BijOn (fun (f : (Fin n → ℝ) → EReal) => fenchelConjugate n f) {f : (Fin n → ℝ) → EReal | LowerSemicontinuous f ∧ ConvexFunction f ∧ ProperConvexFunctionOn Set.univ f} {f : (Fin n → ℝ) → EReal | LowerSemicontinuous f ∧ ConvexFunction f ∧ ProperConvexFunctionOn Set.univ f} ∧ ∀ (f : (Fin n → ℝ) → EReal), LowerSemicontinuous f ∧ ConvexFunction f ∧ ProperConvexFunctionOn Set.univ f → fenchelConjugate n (fenchelConjugate n f) = f

Corollary 12.2.1. The conjugacy operation f ↦ f* (here f* = fenchelConjugate n f) induces a symmetric one-to-one correspondence in the class of all closed proper convex functions on ℝ^n.

theorem fenchelConjugate_eq_of_convexFunctionClosure (n : ℕ) (f : (Fin n → ℝ) → EReal) : fenchelConjugate n (convexFunctionClosure f) = fenchelConjugate n f

Taking the convex-function closure does not change the Fenchel conjugate.

theorem effectiveDomain_if_eq_intrinsicInterior (n : ℕ) (f : (Fin n → ℝ) → EReal) : have C := effectiveDomain Set.univ f; have A := intrinsicInterior ℝ C; have g := fun (x : Fin n → ℝ) => if x ∈ A then f x else ⊤; effectiveDomain Set.univ g = A

The effective domain of x ↦ if x ∈ ri(dom f) then f x else ⊤ is exactly ri(dom f).

theorem convexFunction_if_eq_top_on_compl (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf : ConvexFunction f) (A : Set (Fin n → ℝ)) (hA : Convex ℝ A) : ConvexFunction fun (x : Fin n → ℝ) => if x ∈ A then f x else ⊤

Extending a convex function by ⊤ outside a convex set preserves convexity.

theorem fenchelConjugate_if_eq_sSup_image (n : ℕ) (f : (Fin n → ℝ) → EReal) (A : Set (Fin n → ℝ)) (xStar : Fin n → ℝ) : fenchelConjugate n (fun (x : Fin n → ℝ) => if x ∈ A then f x else ⊤) xStar = sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - f x) '' A)

For g(x)=f(x) on A and g(x)=⊤ outside, g* is the supremum over A.

theorem euclideanRelativeInterior_idem_of_convex (n : ℕ) (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C) : euclideanRelativeInterior n (euclideanRelativeInterior n C) = euclideanRelativeInterior n C

Relative interior is idempotent for convex sets in Euclidean space.

theorem fenchelConjugate_eq_sSup_intrinsicInterior_effectiveDomain (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf : ConvexFunction f) (xStar : Fin n → ℝ) : fenchelConjugate n f xStar = sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - f x) '' intrinsicInterior ℝ (effectiveDomain Set.univ f))

Corollary 12.2.2. For a convex function f on ℝ^n, one can compute the Fenchel conjugate f*(x*) = sup_x (⟪x, x*⟫ - f x) by restricting to points x in ri (dom f). Here f* = fenchelConjugate n f, dom f = effectiveDomain Set.univ f, and ri = intrinsicInterior ℝ.

def SatisfiesGeneralizedFenchelInequality (n : ℕ) (p : ((Fin n → ℝ) → EReal) × ((Fin n → ℝ) → EReal)) : Prop

Text 12.2.2: A pair of functions (f, g) : (ℝ^n → [-∞, ∞]) × (ℝ^n → [-∞, ∞]) satisfies the generalized Fenchel inequality if ⟪x, y⟫ ≤ f x + g y for all x, y ∈ ℝ^n.

Equations

• SatisfiesGeneralizedFenchelInequality n p = ∀ (x y : Fin n → ℝ), ↑(x ⬝ᵥ y) ≤ p.1 x + p.2 y

@[reducible, inline]

abbrev GeneralizedFenchelPairs (n : ℕ) : Type

Text 12.2.2: The set 𝓦 of all pairs (f, g) satisfying the generalized Fenchel inequality.

Equations

• GeneralizedFenchelPairs n = { p : ((Fin n → ℝ) → EReal) × ((Fin n → ℝ) → EReal) // SatisfiesGeneralizedFenchelInequality n p }

theorem satisfiesGeneralizedFenchelInequality_conjugate_le_snd (n : ℕ) {f g : (Fin n → ℝ) → EReal} (h : SatisfiesGeneralizedFenchelInequality n (f, g)) (y : Fin n → ℝ) : fenchelConjugate n f y ≤ g y

From the generalized Fenchel inequality for (f, g), we get the pointwise bound f* ≤ g.

theorem satisfiesGeneralizedFenchelInequality_no_bot (n : ℕ) {f g : (Fin n → ℝ) → EReal} (h : SatisfiesGeneralizedFenchelInequality n (f, g)) : (∀ (x : Fin n → ℝ), f x ≠ ⊥) ∧ ∀ (y : Fin n → ℝ), g y ≠ ⊥

A generalized Fenchel pair cannot take the value ⊥ in either component.

theorem generalizedFenchelPairs_exists_fst_ne_top_of_isMin (n : ℕ) (p : GeneralizedFenchelPairs n) (hpmin : IsMin p) : ∃ (x : Fin n → ℝ), (↑p).1 x ≠ ⊤

A minimal generalized Fenchel pair has some point where the first component is not ⊤.

theorem generalizedFenchelPairs_exists_snd_ne_top_of_isMin (n : ℕ) (p : GeneralizedFenchelPairs n) (hpmin : IsMin p) : ∃ (y : Fin n → ℝ), (↑p).2 y ≠ ⊤

A minimal generalized Fenchel pair has some point where the second component is not ⊤.

theorem satisfiesGeneralizedFenchelInequality_swap (n : ℕ) {f g : (Fin n → ℝ) → EReal} (h : SatisfiesGeneralizedFenchelInequality n (f, g)) : SatisfiesGeneralizedFenchelInequality n (g, f)

Under the generalized Fenchel inequality, swapping the pair preserves the property.

theorem fenchelConjugate_ne_bot_of_exists_ne_top (n : ℕ) (f : (Fin n → ℝ) → EReal) (h : ∃ (x0 : Fin n → ℝ), f x0 ≠ ⊤) (y : Fin n → ℝ) : fenchelConjugate n f y ≠ ⊥

If f has no ⊥ values and is not identically ⊤, then f* is never ⊥.

theorem satisfiesGeneralizedFenchelInequality_self_conjugate (n : ℕ) {f : (Fin n → ℝ) → EReal} (hf_bot : ∀ (x : Fin n → ℝ), f x ≠ ⊥) (hf_top : ∃ (x0 : Fin n → ℝ), f x0 ≠ ⊤) : SatisfiesGeneralizedFenchelInequality n (f, fenchelConjugate n f)

Fenchel's inequality: the pair (f, f*) satisfies the generalized Fenchel inequality.

theorem generalizedFenchelPairs_isMin_iff_mutuallyConjugate (n : ℕ) (p : GeneralizedFenchelPairs n) : IsMin p ↔ (↑p).2 = fenchelConjugate n (↑p).1 ∧ (↑p).1 = fenchelConjugate n (↑p).2

Text 12.2.2: For 𝓦 the set of pairs satisfying the generalized Fenchel inequality, ordered by (f', g') ≼ (f, g) meaning f' ≤ f and g' ≤ g pointwise, a pair is a minimal element of 𝓦 if and only if f and g are mutually conjugate, i.e. g = f^* and f = g^* (here f^* is fenchelConjugate).

theorem fenchel_inequality (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf : ProperConvexFunctionOn Set.univ f) (x xStar : Fin n → ℝ) : ↑(x ⬝ᵥ xStar) ≤ f x + fenchelConjugate n f xStar

Text 12.2.3 (Fenchel's inequality): For any proper convex function f on ℝ^n and its conjugate f*, the inequality ⟪x, x*⟫ ≤ f x + f*(x*) holds for every x ∈ ℝ^n and every x* ∈ ℝ^n. Here the conjugate f* is represented by fenchelConjugate n f.

theorem fenchelConjugate_indicatorFunction_eq_sSup_dotProduct_image (n : ℕ) (L : Submodule ℝ (Fin n → ℝ)) (xStar : Fin n → ℝ) : fenchelConjugate n (indicatorFunction ↑L) xStar = sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar)) '' ↑L)

The Fenchel conjugate of the indicator of a set is the supremum of the dot product over that set.

theorem dotProduct_smul_left_real {n : ℕ} (a : ℝ) (y xStar : Fin n → ℝ) : a • y ⬝ᵥ xStar = a * y ⬝ᵥ xStar

Scaling the left argument scales the dot product.

theorem sSup_dotProduct_image_eq_zero_of_forall_mem_eq_zero {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) (xStar : Fin n → ℝ) (h : ∀ x ∈ L, x ⬝ᵥ xStar = 0) : sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar)) '' ↑L) = 0

If xStar is orthogonal to every x ∈ L, then the supremum of ⟪x,xStar⟫ over L is 0.

theorem sSup_dotProduct_image_eq_top_of_exists_mem_ne_zero {n : ℕ} (L : Submodule ℝ (Fin n → ℝ)) (xStar : Fin n → ℝ) (h : ∃ y ∈ L, y ⬝ᵥ xStar ≠ 0) : sSup ((fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar)) '' ↑L) = ⊤

If some y ∈ L has nonzero dot product with xStar, then the supremum over L is +∞.

theorem fenchelConjugate_indicatorFunction_submodule (n : ℕ) (L : Submodule ℝ (Fin n → ℝ)) : fenchelConjugate n (indicatorFunction ↑L) = indicatorFunction {xStar : Fin n → ℝ | ∀ x ∈ L, x ⬝ᵥ xStar = 0}

Text 12.2.3 (indicator function of a subspace): Let f be the indicator function of a subspace L of ℝ^n, i.e. f(x) = δ(x | L). Then the conjugate function f* is the indicator function of the orthogonal complement L^{⊥} (the set of vectors x* such that ⟪x, x*⟫ = 0 for all x ∈ L), denoted δ(· | L^{⊥}).