noncomputable def fenchelConjugate (n : ℕ) (f : (Fin n → ℝ) → EReal) : (Fin n → ℝ) → EReal

Defn 12.2: The conjugate f* of a function f on ℝ^n is the function on ℝ^n defined by f*(x*) = sup_x (⟪x, x*⟫ - f x) = - inf_x (f x - ⟪x, x*⟫).

Equations

• fenchelConjugate n f xStar = sSup (Set.range fun (x : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - f x)

theorem fenchelConjugate_antitone (n : ℕ) : Antitone fun (f : (Fin n → ℝ) → EReal) => fenchelConjugate n f

Text 12.2.1: If f₁ and f₂ are functions on ℝ^n satisfying f₁ x ≤ f₂ x for every x, then their conjugates satisfy the reverse inequality: f₁*(x*) ≥ f₂*(x*) for every x*.

theorem fenchelConjugate_eq_iSup (n : ℕ) (f : (Fin n → ℝ) → EReal) (xStar : Fin n → ℝ) : fenchelConjugate n f xStar = ⨆ (x : Fin n → ℝ), ↑(x ⬝ᵥ xStar) - f x

fenchelConjugate rewritten as a pointwise iSup (over Set.range).

theorem continuous_dotProduct_const {n : ℕ} (x : Fin n → ℝ) : Continuous fun (xStar : Fin n → ℝ) => x ⬝ᵥ xStar

The dot product with a fixed vector is continuous.

theorem lowerSemicontinuous_dotProduct_sub_const {n : ℕ} (x : Fin n → ℝ) (c : EReal) : LowerSemicontinuous fun (xStar : Fin n → ℝ) => ↑(x ⬝ᵥ xStar) - c

Lower semicontinuity of the affine pieces xStar ↦ ⟪x, xStar⟫ - c used in fenchelConjugate.

theorem fenchelConjugate_le_coe_iff_affine_le (n : ℕ) (f : (Fin n → ℝ) → EReal) (b : Fin n → ℝ) (μ : ℝ) : fenchelConjugate n f b ≤ ↑μ ↔ ∀ (x : Fin n → ℝ), ↑(x ⬝ᵥ b - μ) ≤ f x

f*(b) ≤ μ iff the affine function x ↦ ⟪x,b⟫ - μ is pointwise below f.

theorem affineMap_exists_dotProduct_sub {n : ℕ} (h : (Fin n → ℝ) →ᵃ[ℝ] ℝ) : ∃ (b : Fin n → ℝ) (β : ℝ), ∀ (x : Fin n → ℝ), h x = x ⬝ᵥ b - β

Any affine map h : ℝ^n → ℝ can be written as x ↦ ⟪x,b⟫ - β.

theorem clConv_le (n : ℕ) (f : (Fin n → ℝ) → EReal) : clConv n f ≤ f

clConv n f is pointwise bounded above by f.

theorem affine_le_clConv (n : ℕ) (f : (Fin n → ℝ) → EReal) (h : (Fin n → ℝ) →ᵃ[ℝ] ℝ) (hh : ∀ (y : Fin n → ℝ), ↑(h y) ≤ f y) (x : Fin n → ℝ) : ↑(h x) ≤ clConv n f x

Any affine minorant of f is pointwise below clConv n f.

theorem EReal.eq_of_forall_le_coe_iff {a b : EReal} (h : ∀ (μ : ℝ), a ≤ ↑μ ↔ b ≤ ↑μ) : a = b

Two EReal values are equal if they have the same real upper bounds.

theorem fenchelConjugate_closedConvex (n : ℕ) (f : (Fin n → ℝ) → EReal) : LowerSemicontinuous (fenchelConjugate n f) ∧ ConvexFunction (fenchelConjugate n f)

The Fenchel conjugate is always closed and convex.

theorem sub_eq_sSup_image_sub_of_le (x : ℝ) (a : EReal) : ↑x - a = sSup ((fun (β : ℝ) => ↑(x - β)) '' {β : ℝ | a ≤ ↑β})

For a real x and a : EReal, x - a is the supremum of x - β over real β with a ≤ β.

theorem fenchelConjugate_biconjugate_eq_clConv (n : ℕ) (f : (Fin n → ℝ) → EReal) : fenchelConjugate n (fenchelConjugate n f) = clConv n f

The Fenchel biconjugate coincides with clConv.

theorem fenchelConjugate_clConv_eq (n : ℕ) (f : (Fin n → ℝ) → EReal) : fenchelConjugate n (clConv n f) = fenchelConjugate n f

The conjugate of clConv agrees with the conjugate.

theorem clConv_eq_const_top_of_forall_eq_top {n : ℕ} (f : (Fin n → ℝ) → EReal) (hf : ∀ (x : Fin n → ℝ), f x = ⊤) : clConv n f = fun (x : Fin n → ℝ) => ⊤

If f is identically ⊤, then clConv n f is identically ⊤.

theorem proper_fenchelConjugate_of_proper (n : ℕ) {f : (Fin n → ℝ) → EReal} (hf : ProperConvexFunctionOn Set.univ f) : ProperConvexFunctionOn Set.univ (fenchelConjugate n f)

A proper convex function has a proper Fenchel conjugate.

theorem fenchelConjugate_proper_iff (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf : ConvexFunction f) : ProperConvexFunctionOn Set.univ (fenchelConjugate n f) ↔ ProperConvexFunctionOn Set.univ f

Properness is preserved by Fenchel conjugation (for convex functions).

theorem fenchelConjugate_closedConvex_proper_iff_and_biconjugate (n : ℕ) (f : (Fin n → ℝ) → EReal) (hf : ConvexFunction f) : (LowerSemicontinuous (fenchelConjugate n f) ∧ ConvexFunction (fenchelConjugate n f)) ∧ (ProperConvexFunctionOn Set.univ (fenchelConjugate n f) ↔ ProperConvexFunctionOn Set.univ f) ∧ fenchelConjugate n (clConv n f) = fenchelConjugate n f ∧ fenchelConjugate n (fenchelConjugate n f) = clConv n f

Theorem 12.2. Let f be a convex function. Then its conjugate f* (here represented by fenchelConjugate n f) is a closed convex function, and it is proper if and only if f is proper. Moreover, the conjugate of the closure equals the conjugate, and the biconjugate equals the closure: (cl f)^* = f^* and f^{**} = cl f (here cl f is represented by clConv n f).

theorem isClosed_epigraph_univ_of_lowerSemicontinuous {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf : LowerSemicontinuous f) : IsClosed (epigraph Set.univ f)

Lower semicontinuity implies closedness of the book's epigraph epigraph univ f.

theorem exists_affineMap_strictly_above_below_point_ereal {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_closed : LowerSemicontinuous f) (hf_proper : ProperConvexFunctionOn Set.univ f) (x0 : Fin n → ℝ) (μ0 : ℝ) : ↑μ0 < f x0 → ∃ (h : (Fin n → ℝ) →ᵃ[ℝ] ℝ), (∀ (y : Fin n → ℝ), ↑(h y) ≤ f y) ∧ μ0 < h x0

Supporting affine minorant for a closed proper convex EReal-valued function: if (μ0 : EReal) < f x0, then there is an affine h with h ≤ f and μ0 < h x0.

theorem clConv_eq_of_closedProperConvex {n : ℕ} {f : (Fin n → ℝ) → EReal} (hf_closed : LowerSemicontinuous f) (hf_proper : ProperConvexFunctionOn Set.univ f) : clConv n f = f

A closed proper convex function agrees with its clConv envelope.