The Legendre transformation #

Let f be a convex function, differentiable on an open set C. Its Legendre conjugate is the pair (D, g) with D = ∇f(C) the image of the gradient mapping and g y = ⟨x, y⟩ - f x for any x with ∇f x = y. The value of g does not depend on which such x is chosen, and g is nothing but the restriction of the Fenchel conjugate f* to D; in particular D ⊆ dom f*.

Main results #

legendreDom — the set D, the image of the gradient mapping, with legendreDom_subset_dom_conj for D ⊆ dom f*.
conj_eq_of_hasGradientAt — f*(∇f x) = ⟨x, ∇f x⟩ - f x: both the formula for g and, at a stroke, its well-definedness (Theorem 26.4 in [^1]).

Implementation notes #

There is deliberately no legendreConj definition: y ↦ ⟨(∇f)⁻¹ y, y⟩ - f ((∇f)⁻¹ y) would need a choice function and would then have to be proved equal to conj B f on D anyway, and conj_eq_of_hasGradientAt is that equality without the detour.

References #

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §26.

source

theorem Tdaf.ConvexAnalysis.HasGradientAt.exists_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {x : E} {y : StrongDual ℝ E} (h : HasGradientAt f y x) :

∃ (r : ℝ), f x = ↑r

A function is finite wherever it has a gradient.

source

theorem Tdaf.ConvexAnalysis.HasGradientAt.add_conj_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {x : E} {y : StrongDual ℝ E} (hf : ConvexFn f) (h : HasGradientAt f y x) :

f x + conj (topDualPairing ℝ E).flip f y = ↑(y x)

Where f is differentiable, Fenchel's inequality holds with equality at (x, ∇f x).

source

theorem Tdaf.ConvexAnalysis.conj_eq_of_hasGradientAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {x : E} {y : StrongDual ℝ E} (hf : ConvexFn f) (h : HasGradientAt f y x) {r : ℝ} (hr : f x = ↑r) :

conj (topDualPairing ℝ E).flip f y = ↑(y x - r)

The Legendre conjugate at ∇f x is f* at ∇f x, given by the formula ⟨x, ∇f x⟩ - f x.

source

theorem Tdaf.ConvexAnalysis.sub_eq_sub_of_hasGradientAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {y : StrongDual ℝ E} (hf : ConvexFn f) {x₁ x₂ : E} {r₁ r₂ : ℝ} (h₁ : HasGradientAt f y x₁) (h₂ : HasGradientAt f y x₂) (hr₁ : f x₁ = ↑r₁) (hr₂ : f x₂ = ↑r₂) :

y x₁ - r₁ = y x₂ - r₂

Well-definedness: ⟨x, y⟩ - f x is the same for every x with ∇f x = y, because it is f* y. So ∇f need not be one-to-one for g to be single-valued.

source

def Tdaf.ConvexAnalysis.legendreDom {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → EReal) :

Set (StrongDual ℝ E)

The domain D of the Legendre conjugate, the image of the gradient mapping. Every gradient is attained at an interior point of dom f (HasGradientAt.mem_interior_dom), so no interiority side condition is needed here.

Equations