Derivatives of Exponential Laplace-Type Integrals

This theorem identifies the iterated derivatives of a vector-valued Laplace-type integral with weighted moments.

Let $E$ be a finite-dimensional real inner-product space, let $F$ be a complete real normed space, and let $\mu$ be a measure on $E$. Let $g:E\to F$ be strongly measurable almost everywhere with respect to $\mu$, and assume that for every $r\in\mathbb R$ the function $x\mapsto e^{r\|x\|}\|g(x)\|$ is integrable. For every $d\in\mathbb N$, $z\in E$, and $h:\operatorname{Fin}(d)\to E$, define $N(z)=\int e^{\langle z,x\rangle}g(x)\,d\mu(x)$.

The result is a reusable differentiation-under-the-integral statement for exponential moments with values in a complete normed space.

Original Lean declaration header

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

theorem iteratedFDeriv_integral_exp_inner_smul (μ : Measure E) {g : E → F}
    (hg : AEStronglyMeasurable g μ)
    (hgi : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖) * ‖g x‖) μ) (d : ℕ) (z : E)
    (h : Fin d → E) :
    iteratedFDeriv ℝ d (fun z => ∫ x, Real.exp ⟪z, x⟫ • g x ∂μ) z h =
      ∫ x, (Real.exp ⟪z, x⟫ * ∏ j, ⟪x, h j⟫) • g x ∂μ

Module navigation

Module: Analysis/BakryEmery/Tilt/SquareIntegrable.

Next: integrable_exp_mul_norm_of_memLp.

Source excerpt, lines 185–190 · Frozen source 408915f.