Legendre transform

DefinitionLegendre transform#✓fully proved

Let \(d \in \mathbb{N}\), give \(\mathbb{R}^d\) its standard inner product, and let \(\Lambda : \mathbb{R}^d \to [-\infty, \infty]\). The Legendre transform of \(\Lambda\) at \(x \in \mathbb{R}^d\) is the Fenchel conjugate of \(\Lambda\) at the linear functional \(y \mapsto \langle x, y \rangle\), that is, the extended real number \(\Lambda^*(x) = \sup_{y \in \mathbb{R}^d} \big(\langle x, y \rangle - \Lambda(y)\big)\).

noncomputable def legendreTransform {d : ℕ}
    (Λ : EuclideanSpace ℝ (Fin d) → EReal) (x : EuclideanSpace ℝ (Fin d)) : EReal :=
  fenchelConj Λ (innerSL ℝ x)

Uses 1 · Used by 17

Statement usesFenchel conjugate

Used byCramér rate function agrees with the extended conjugate · Cramér rate function · Cramér rate function of a constant law · Convexity of the Cramér rate function · Cramér rate function as a supremum · Extended Fenchel–Young inequality for the Cramér rate function · Nonnegativity of the Legendre transform of the log moment · Lower semicontinuity of the Cramér rate function · The epigraph of the Legendre transform is convex · A finite Legendre transform is convex · Fenchel–Young inequality for the Legendre transform · The Legendre transform is order-reversing · Supremum formula for the Legendre transform · The double Legendre transform lies below the function · The half squared norm is its own Legendre transform · Legendre transform of the zero function at the origin · Legendre transform of the zero function away from the origin

TheoremSupremum formula for the Legendre transform#✓fully proved

Let \(d \in \mathbb{N}\) and let \(\Lambda : \mathbb{R}^d \to [-\infty, \infty]\). For every \(x \in \mathbb{R}^d\), the Legendre transform \(\Lambda^*\) of \(\Lambda\) satisfies \(\Lambda^*(x) = \sup_{l \in \mathbb{R}^d} \big(\langle l, x \rangle - \Lambda(l)\big)\).

theorem legendreTransform_eq_iSup {d : ℕ}
    (Λ : EuclideanSpace ℝ (Fin d) → EReal) (x : EuclideanSpace ℝ (Fin d)) :
    legendreTransform Λ x = ⨆ l, ((⟪l, x⟫_ℝ : ℝ) : EReal) - Λ l

Uses 2 · Used by 9

Statement usesLegendre transform

Proof usesFenchel conjugate

Used byCramér rate function of a constant law · Cramér rate function as a supremum · Lower semicontinuity of the Cramér rate function · The epigraph of the Legendre transform is convex · Fenchel–Young inequality for the Legendre transform · The Legendre transform is order-reversing · The double Legendre transform lies below the function · The half squared norm is its own Legendre transform · Legendre transform of the zero function at the origin

TheoremFenchel–Young inequality for the Legendre transform#✓fully proved

Let \(d \in \mathbb{N}\) and let \(\Lambda : \mathbb{R}^d \to [-\infty, \infty]\), with Legendre transform \(\Lambda^*\). For all \(x, l \in \mathbb{R}^d\), we have \(\langle l, x \rangle - \Lambda(l) \le \Lambda^*(x)\) in \([-\infty, \infty]\).

theorem le_legendreTransform {d : ℕ}
    {Λ : EuclideanSpace ℝ (Fin d) → EReal}
    {x l : EuclideanSpace ℝ (Fin d)} :
    ((⟪l, x⟫_ℝ : ℝ) : EReal) - Λ l ≤ legendreTransform Λ x

Uses 2 · Used by 5

Statement usesLegendre transform

Proof usesSupremum formula for the Legendre transform

Used byExtended Fenchel–Young inequality for the Cramér rate function · Nonnegativity of the Legendre transform of the log moment · The epigraph of the Legendre transform is convex · The half squared norm is its own Legendre transform · Legendre transform of the zero function away from the origin

TheoremThe Legendre transform is order-reversing#✓fully proved

Let \(d \in \mathbb{N}\) and let \(\Lambda_1, \Lambda_2 : \mathbb{R}^d \to [-\infty, \infty]\), with Legendre transforms \(\Lambda_1^*\) and \(\Lambda_2^*\). If \(\Lambda_1(y) \le \Lambda_2(y)\) for every \(y \in \mathbb{R}^d\), then \(\Lambda_2^*(x) \le \Lambda_1^*(x)\) for every \(x \in \mathbb{R}^d\).

theorem legendreTransform_antitone {d : ℕ}
    {Λ₁ Λ₂ : EuclideanSpace ℝ (Fin d) → EReal} (h : ∀ x, Λ₁ x ≤ Λ₂ x)
    {x : EuclideanSpace ℝ (Fin d)} :
    legendreTransform Λ₂ x ≤ legendreTransform Λ₁ x

Uses 2

Statement usesLegendre transform

Proof usesSupremum formula for the Legendre transform

TheoremThe epigraph of the Legendre transform is convex#✓fully proved

Let \(d \in \mathbb{N}\) and let \(\Lambda : \mathbb{R}^d \to [-\infty, \infty]\), with Legendre transform \(\Lambda^*\). Then the set \(\{(x, t) \in \mathbb{R}^d \times \mathbb{R} : \Lambda^*(x) \le t\}\) is convex.

theorem convex_epi_legendreTransform {d : ℕ}
    (Λ : EuclideanSpace ℝ (Fin d) → EReal) :
    Convex ℝ {p : EuclideanSpace ℝ (Fin d) × ℝ |
      legendreTransform Λ p.1 ≤ (p.2 : EReal)}

Uses 3 · Used by 2

Statement usesLegendre transform

Proof usesFenchel–Young inequality for the Legendre transform · Supremum formula for the Legendre transform

Used byConvexity of the Cramér rate function · A finite Legendre transform is convex

TheoremA finite Legendre transform is convex#✓fully proved

Let \(d \in \mathbb{N}\) and let \(\Lambda : \mathbb{R}^d \to [-\infty, \infty]\), with Legendre transform \(\Lambda^*\). If \(\Lambda^*(x)\) is a real number for every \(x \in \mathbb{R}^d\), then \(\Lambda^*\), viewed as a function \(\mathbb{R}^d \to \mathbb{R}\), is convex on \(\mathbb{R}^d\).

theorem convexOn_legendreTransform {d : ℕ}
    {Λ : EuclideanSpace ℝ (Fin d) → EReal}
    (hfinite : ∀ x, legendreTransform Λ x ≠ ⊤ ∧ legendreTransform Λ x ≠ ⊥) :
    ConvexOn ℝ Set.univ (fun x => (legendreTransform Λ x).toReal)

Uses 2

Statement usesLegendre transform

Proof usesThe epigraph of the Legendre transform is convex

TheoremThe double Legendre transform lies below the function#✓fully proved

Let \(d \in \mathbb{N}\) and let \(\Lambda : \mathbb{R}^d \to [-\infty, \infty]\) be a function that never takes the value \(-\infty\), with Legendre transform \(\Lambda^*\). Then the Legendre transform \(\Lambda^{**}\) of \(\Lambda^*\) satisfies \(\Lambda^{**}(x) \le \Lambda(x)\) for every \(x \in \mathbb{R}^d\).

The proof bounds \(\Lambda^{**}\) by the Fenchel biconjugate of \(\Lambda\).

theorem legendreTransform_legendreTransform_le {d : ℕ}
    {Λ : EuclideanSpace ℝ (Fin d) → EReal}
    (hnotbot : ∀ x, Λ x ≠ ⊥) {x : EuclideanSpace ℝ (Fin d)} :
    legendreTransform (legendreTransform Λ) x ≤ Λ x

Uses 5

Statement usesLegendre transform

Proof usesThe biconjugate lies below the function · Fenchel biconjugate · Fenchel conjugate · Supremum formula for the Legendre transform

TheoremThe half squared norm is its own Legendre transform#✓fully proved

Let \(d \in \mathbb{N}\) and let \(q : \mathbb{R}^d \to [-\infty, \infty]\) be \(q(y) = \|y\|^2 / 2\), where \(\|\cdot\|\) is the Euclidean norm. Its Legendre transform \(q^*\) satisfies \(q^*(x) = \|x\|^2 / 2\) for every \(x \in \mathbb{R}^d\); in particular every value of \(q^*\) is finite.

theorem legendreTransform_norm_sq_div_two {d : ℕ} (x : EuclideanSpace ℝ (Fin d)) :
    legendreTransform (fun y : EuclideanSpace ℝ (Fin d) => ((‖y‖ ^ 2 / 2 : ℝ) : EReal)) x
      = ((‖x‖ ^ 2 / 2 : ℝ) : EReal)

Uses 3

Statement usesLegendre transform

Proof usesFenchel–Young inequality for the Legendre transform · Supremum formula for the Legendre transform

TheoremLegendre transform of the zero function at the origin#✓fully proved

Let \(d \in \mathbb{N}\) and let \(\Lambda : \mathbb{R}^d \to [-\infty, \infty]\) be the zero function. Its Legendre transform \(\Lambda^*\) satisfies \(\Lambda^*(0) = 0\).

theorem legendreTransform_zero {d : ℕ} :
    legendreTransform (fun _ : EuclideanSpace ℝ (Fin d) => (0 : EReal)) 0 = 0

Uses 2 · Used by 1

Statement usesLegendre transform

Proof usesSupremum formula for the Legendre transform

Used byCramér rate function of a constant law

TheoremLegendre transform of the zero function away from the origin#✓fully proved

Let \(d \in \mathbb{N}\) and let \(\Lambda : \mathbb{R}^d \to [-\infty, \infty]\) be the zero function. Its Legendre transform \(\Lambda^*\) satisfies \(\Lambda^*(x) = +\infty\) for every nonzero \(x \in \mathbb{R}^d\).

theorem legendreTransform_zero_of_ne {d : ℕ} {x : EuclideanSpace ℝ (Fin d)} (hx : x ≠ 0) :
    legendreTransform (fun _ : EuclideanSpace ℝ (Fin d) => (0 : EReal)) x = ⊤

Uses 2 · Used by 1

Statement usesLegendre transform

Proof usesFenchel–Young inequality for the Legendre transform

Used byCramér rate function of a constant law

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.