Pointwise Legendre First Variation

This is a pointwise first-variation formula for the Legendre transform under a bounded continuous perturbation.

Let $E$ be a finite-dimensional real inner-product space and let $\phi:E\to\overline{\mathbb{R}}$ be a proper lower-semicontinuous potential. Let $y$ lie in the interior of the finite domain of $\phi^*$, and assume $q\mapsto(\phi^*(q)).toReal$ is differentiable at $y$. Let $b:E\to\mathbb{R}$ be continuous and assume $|b|$ is bounded above. Then the map

has derivative at $0$ equal to

Here $(\phi+t b)(z)$ denotes $\phi(z)+(t b(z):\overline{\mathbb{R}})$. No differentiability or global finiteness of $\phi$ is assumed.

Original Lean declaration header

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

theorem hasDerivAt_legendre_add_smul_of_dualDifferentiable
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E]
    (φ : E → EReal) (hφ : ProperPotential φ)
    (hlsc : LowerSemicontinuous φ) (y : E)
    (hy : y ∈ interior {q : E | legendre φ q ≠ ⊤})
    (hd : DifferentiableAt ℝ (fun q => (legendre φ q).toReal) y)
    (b : E → ℝ) (hb : Continuous b)
    (hbounded : BddAbove (Set.range fun z : E => |b z|)) :
    HasDerivAt
      (fun t : ℝ =>
        (legendre (fun z : E => φ z + ((t * b z : ℝ) : EReal)) y).toReal)
      (-b (gradient (fun q => (legendre φ q).toReal) y)) 0

Module navigation

Module: Analysis/Convex/LegendreVariation/Derivative.

Definition modules: Analysis/Convex/Legendre.

Supporting theorems: exists_delta_nearMaximizer_norm_sub_gradient_lt, exists_legendre_maximizer_with_gradient_identity, legendre_bounded_perturbation_finite_curve.

Previous: exists_delta_nearMaximizer_norm_sub_gradient_lt.

Source excerpt, lines 245–257 · Frozen source 408915f.