Lipschitz Representative of a Finite Legendre Transform

This shows that bounded effective-domain slopes yield a Lipschitz real representative of the Legendre transform.

Let $E$ be a real inner-product space, let $q:E\to\overline{\mathbb R}$, let $L\in[0,\infty)$, and let $\psi:E\to\mathbb R$. Assume:

1. $q(y)\neq-\infty$ for every $y$;
2. whenever $q(y)\neq+\infty$, one has $y\in\overline B(0,L)$;
3. $\operatorname{Leg}(q)(x)=\psi(x)$ as an extended-real equality for every $x$.

Then ψ is $L$-Lipschitz, expressed by LipschitzWith L ψ.

Only finite values of $q$ are converted using toReal; the supremum itself remains an extended-real supremum.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem lipschitzWith_real_legendre
    (q : E → EReal) (L : NNReal) (ψ : E → ℝ)
    (hbot : ∀ y, q y ≠ ⊥)
    (hdom : ∀ y, q y ≠ ⊤ → y ∈ closedBall (0 : E) (L : ℝ))
    (hψ : ∀ x, legendre q x = (ψ x : EReal)) :
    LipschitzWith L ψ

Module navigation

Module: Analysis/Convex/BoundedConjugate.

Definition modules: Analysis/Convex/Legendre.

Previous: real_convexOn_legendre.

Source excerpt, lines 178–183 · Frozen source 408915f.