Finite Legendre Curve Under Bounded Perturbations

This gives a finite real-valued perturbation curve for the Legendre transform.

Let $\phi:E\to\overline{\mathbb R}$ be proper and let $y\in E$ satisfy $\operatorname{Leg}(\phi)(y)\neq+\infty$. Let $b:E\to\mathbb R$, let $M\geq0$, and assume $|b(z)|\leq M$ for every $z$. For every $t\in\mathbb R$, define

Then $\psi_t$ is neither $+\infty$ nor $-\infty$, and

This is the finite-value consequence of the extended-real perturbation estimate and is useful for treating Legendre variations as real curves.

Original Lean declaration header

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

theorem legendre_bounded_perturbation_finite_curve
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (φ : E → EReal) (hφ : ProperPotential φ) (y : E)
    (hy : legendre φ y ≠ ⊤)
    (b : E → ℝ) (M : ℝ) (hM : 0 ≤ M)
    (hb : ∀ z : E, |b z| ≤ M) :
    ∀ t : ℝ,
      let ψ := legendre (fun z : E => φ z + ((t * b z : ℝ) : EReal)) y
      ψ ≠ ⊤ ∧ ψ ≠ ⊥ ∧
        |ψ.toReal - (legendre φ y).toReal| ≤ |t| * M

Module navigation

Module: Analysis/Convex/LegendreVariation/Perturbation.

Definition modules: Analysis/Convex/Legendre.

Supporting theorems: legendre_bounded_perturbation.

Previous: legendre_bounded_perturbation.

Source excerpt, lines 127–136 · Frozen source 408915f.