Bounded Perturbation of the Extended-Real Legendre Transform

This states the uniform perturbation bound for the actual extended-real Legendre transform.

Let $E$ be a real inner-product space, let $\phi:E\to\overline{\mathbb R}$ be a proper potential, and let $b:E\to\mathbb R$. If $M\geq0$ and $|b(z)|\leq M$ for every $z$, then for every $t\in\mathbb R$ and $q\in E$,

The inequalities hold in EReal, including infinite values; no convexity or global finiteness of $\phi$ is assumed. This gives a direct stability estimate for bounded perturbations of the conjugate.

Original Lean declaration header

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

theorem legendre_bounded_perturbation
    (φ : E → EReal) (hφ : ProperPotential φ)
    (b : E → ℝ) (M : ℝ) (hM : 0 ≤ M) (hb : ∀ z : E, |b z| ≤ M) :
    ∀ (t : ℝ) (q : E),
      legendre φ q - ((|t| * M : ℝ) : EReal) ≤
          legendre (fun z : E => φ z + ((t * b z : ℝ) : EReal)) q ∧
        legendre (fun z : E => φ z + ((t * b z : ℝ) : EReal)) q ≤
          legendre φ q + ((|t| * M : ℝ) : EReal)

Module navigation

Module: Analysis/Convex/LegendreVariation/Perturbation.

Definition modules: Analysis/Convex/Legendre.

Next: legendre_bounded_perturbation_finite_curve.

Source excerpt, lines 64–71 · Frozen source 408915f.