Conjugate Maximizer Equals Dual Gradient

This is the identification part of the dual-differentiability argument from Berman–Berndtsson, arXiv:1207.6128v1, Lemma 2.7 and Appendix 6, and is used for the first-variation framework of Cordero-Erausquin–Klartag, arXiv:1304.0630v1.

Let $E$ be a finite-dimensional real inner-product space and let $\varphi:E\to[-\infty,\infty]$ be a ProperPotential. Let $y$ lie in the interior of the set where the Legendre transform $\varphi^*$ is not $+\infty$, and assume $q\mapsto(\varphi^*(q)).\operatorname{toReal}$ is differentiable at $y$. If $z\in E$ satisfies

then

The declaration is conjugate_maximizer_eq_gradient_readable. The primal potential need not be convex, differentiable, nonnegative, or finite everywhere; existence of a maximizer is not asserted.

Original Lean declaration header

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

theorem conjugate_maximizer_eq_gradient
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E]
    (φ : E → EReal) (hφ : FunctionalInequalities.Analysis.ProperPotential φ)
    {y : E} (hy : y ∈ interior {q | FunctionalInequalities.Analysis.legendre φ q ≠ ⊤})
    (hd : DifferentiableAt ℝ
      (fun q => (FunctionalInequalities.Analysis.legendre φ q).toReal) y) :
    ∀ z : E,
      (inner ℝ z y : EReal) - φ z = FunctionalInequalities.Analysis.legendre φ y →
      z = gradient (fun q => (FunctionalInequalities.Analysis.legendre φ q).toReal) y

Module navigation

Module: Analysis/Convex/LegendreVariation/Attainment.

Definition modules: Analysis/Convex/Legendre.

Next: exists_coercive_tilt_of_mem_interior_legendre_domain.

Source excerpt, lines 43–52 · Frozen source 408915f.