First Variation of the Conjugate Partition Function

This formalizes the integrated first-variation formula (42) in the proof of Theorem 2 of Cordero–Klartag (arXiv:1304.0630v1).

Let $E$ be finite-dimensional with Borel structure, let $q$ be proper and lower semicontinuous, and let $\psi:E\to\mathbb{R}$ satisfy $q^*(x)=\psi(x)$ for every $x$. Assume $\psi$ is $L$-Lipschitz for some $L\in[0,\infty)$ and $e^{-\psi}$ is integrable with respect to Lebesgue measure. Let $b:E\to\mathbb{R}$ be continuous and suppose $|b(z)|\le M$ for some $M\in\mathbb{R}$ and every $z$. Then

has derivative at $0$ equal to

The gradient is the a.e. gradient represented by gradient; no stronger smoothness is asserted.

Original Lean declaration header

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

theorem hasDerivAt_integral_exp_neg_legendre_add_smul (q : E → EReal) (hq : ProperPotential q)
    (hlsc : LowerSemicontinuous q) (ψ : E → ℝ) (hψ : ∀ x, legendre q x = (ψ x : EReal))
    {L : NNReal} (hlip : LipschitzWith L ψ)
    (hint : Integrable (fun x => Real.exp (-ψ x)) (volume : Measure E))
    (b : E → ℝ) (hb : Continuous b) {M : ℝ} (hM : ∀ z, |b z| ≤ M) :
    HasDerivAt
      (fun t : ℝ => ∫ x, Real.exp (-(legendre (fun z => q z + ((t * b z : ℝ) : EReal)) x).toReal)
        ∂(volume : Measure E))
      (∫ x, Real.exp (-ψ x) * b (gradient ψ x) ∂(volume : Measure E)) 0

Module navigation

Module: KLS/CEK/PartitionVariation.

Definition modules: Analysis/Convex/Legendre.

Supporting theorems: hasDerivAt_legendre_add_smul_of_dualDifferentiable, legendre_bounded_perturbation_finite_curve.

Source excerpt, lines 31–39 · Frozen source 408915f.