Derivative of the Graph Logarithmic Integral at Zero

This auxiliary lemma identifies a local scalar derivative of a logarithmic exponential integral.

Let $n\in\mathbb N$, $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)), $\mu$ a probability measure on $E$, and $f:E\to\mathbb R$ measurable. Let $G(x)=(f(x),x)$ in the Euclidean space indexed by $\operatorname{Option}(\operatorname{Fin}n)$, and put $\Gamma=G_*\mu$ (Measure.map). Assume $r>0$ and $y\mapsto e^{r\|y\|}\in L^1(\Gamma)$.

For every $z\in E$ with $\|z\|<r$, the real function $w\mapsto\log\int e^{wf(x)+\langle z,x\rangle}\,d\mu(x)$ has derivative at $w=0$ equal to the tilted average $F_f(z)$ (tiltAverage):

The formal conclusion is HasDerivAt, so it includes existence of the derivative. This is a local derivative interface under a graph-law exponential norm moment.

Original Lean declaration header

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

private theorem graph_log_integral_hasDerivAt_zero {n : ℕ}
    (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : Measurable f) {r : ℝ} (_hr : 0 < r)
    (hexp : Integrable (fun y : EuclideanSpace ℝ (Option (Fin n)) => Real.exp (r * ‖y‖))
      (μ.map (fun x : EuclideanSpace ℝ (Fin n) =>
        (WithLp.toLp 2 fun o => Option.elim o (f x) fun j => x j :
          EuclideanSpace ℝ (Option (Fin n))))))
    (z : EuclideanSpace ℝ (Fin n)) (hz : ‖z‖ < r) :
    HasDerivAt (fun w : ℝ => Real.log (∫ x, Real.exp (w * f x + ⟪z, x⟫) ∂μ))
      (tiltAverage μ f z) 0

Module navigation

Module: KLS/BKL/Suspension/Derivatives.

Definition modules: Analysis/BakryEmery/Tilt/Basic.

Next: joint_first_derivative_of_radii.

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