Convergence of Truncated Laplace Derivatives

This statement proves convergence of the iterated derivatives of Laplace transforms of ball-conditioned measures.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure, and let $\nu$ be a probability measure on $E$. Let $r>0$ and assume

For each $d\in\mathbb N$, define the Laplace transform of the conditional measure on the closed ball $\overline B(0,R)$ by

and let $L(z)=\int e^{\langle z,x\rangle}\,d\nu(x)$. Then, as $R\to\infty$ through natural numbers,

Here convergence is in the norm of the corresponding iterated derivative spaces. This is the moment-tensor convergence statement used in truncation arguments for cumulants.

Original Lean declaration header

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

theorem tendsto_iteratedFDeriv_laplace_cond_closedBall (ν : Measure E) [IsProbabilityMeasure ν]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) ν) (d : ℕ) :
    Tendsto (fun R : ℕ => iteratedFDeriv ℝ d
        (fun z => ∫ x, Real.exp ⟪z, x⟫ ∂(ν[|Metric.closedBall (0 : E) R])) 0) atTop
      (𝓝 (iteratedFDeriv ℝ d (fun z => ∫ x, Real.exp ⟪z, x⟫ ∂ν) 0))

Module navigation

Module: Analysis/BakryEmery/Cumulant/Truncation.

Supporting theorems: norm_iteratedFDeriv_laplace_cond_sub_le.

Previous: norm_iteratedFDeriv_laplace_cond_sub_le · Next: cumulant_eq_taylorComp_cond.

Source excerpt, lines 118–122 · Frozen source 408915f.