Smoothness of the Log-Laplace Transform on a Ball

This is the local smoothness statement for the log-Laplace transform, corresponding to the finite-and-smooth assertion in Bizeul–Klartag–Lehec, p. 29.

Let $E$ be a finite-dimensional real inner-product space with its Borel structure. Let $\mu$ be a finite nonzero measure on $E$, and let $r>0$. Assume

Then the log-Laplace transform $\Lambda_\mu(z)=\log\int e^{\langle z,x\rangle}\,d\mu(x)$ is $C^\infty$ on the open ball $B(0,r)$:

The nonzero condition is represented by the NeZero μ instance, and finiteness by IsFiniteMeasure μ. The conclusion is ContDiffOn ℝ ∞ (logLaplace μ) on the ball.

Original Lean declaration header

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

theorem contDiffOn_logLaplace_ball (μ : Measure E) [IsFiniteMeasure μ] [NeZero μ] {r : ℝ}
    (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ) :
    ContDiffOn ℝ ∞ (logLaplace μ) (Metric.ball 0 r)

Module navigation

Module: Analysis/BakryEmery/Cumulant/Basic.

Previous: norm_coordTensor_taylorTensor_inner_sq_le_of_basis · Next: cumulant_map_linearIsometryEquiv.

Source excerpt, lines 761–763 · Frozen source 408915f.