Local Scalar-Direction Fréchet Derivative of the Suspension Log-Laplace Transform

This auxiliary statement formalizes equation (111) in the suspension argument for Proposition 7.1, p. 28, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $n,N\in\mathbb N$ with $N>0$, and $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)). Let $h_V:$ RegularPotential $V\ a\ b'$: $a,b'>0$, $V$ is smooth with derivatives of polynomial growth, and $a\operatorname{Id}\le D^2V\le b'\operatorname{Id}$. Put $\mu=h_V.\text{law}$, the normalized $e^{-V}$ law. Assume:

1. $\beta>0$ and $f:E\to\mathbb R$ is $C^2$.
2. $\|D(Df)(x)\|\le M$ for every $x$, where $M\in\mathbb R$.
3. $(\beta/\sqrt N)M\le a$.

Set $\sigma_\beta=\sqrt{1+2/\beta^2}$ (sigma) and $\lambda=$ jointLaw $\mu\ f\ \beta\ \sigma_\beta\ N$ on $H=$ JointSpace $N\ n$. Write $z_0$ for the scalar coordinate, $z_i$ for the copy blocks, and $e_0$ for the scalar unit vector. There exists $r>0$ such that every $z\in H$ with $\|z\|<r$ and $z_0=0$ satisfies

Here $D$ is fderiv, $\Lambda_\lambda=$ logLaplace, and $F_f=$ tiltAverage. This supplies the local first-derivative identity for mixed-cumulant calculations; it does not require isotropy or normalization of $f$.

Original Lean declaration header

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

theorem fderiv_logLaplace_jointLaw_none {n N : ℕ} (hN : 0 < N) (V : EuclideanSpace ℝ (Fin n) → ℝ)
    {a b' : ℝ} (hV : KLS.RegularPotential V a b') {f : EuclideanSpace ℝ (Fin n) → ℝ} {M β : ℝ}
    (hβ : 0 < β) (hf : ContDiff ℝ 2 f) (hfM : ∀ x, ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ M)
    (h110 : β / Real.sqrt N * M ≤ a) :
    ∃ r > 0, ∀ z : JointSpace N n, ‖z‖ < r → z none = 0 →
      fderiv ℝ (logLaplace (jointLaw (hV.law : Measure _) f β (sigma β) N)) z
          (EuclideanSpace.single none 1) =
        (sigma β * Real.sqrt N)⁻¹ *
          ∑ i, tiltAverage (hV.law : Measure _) f (WithLp.toLp 2 fun j => z (some (i, j)))

Module navigation

Module: KLS/BKL/Suspension/Derivatives.

Definition modules: Analysis/BakryEmery/Cumulant/Basic, KLS/BKL/Suspension/Law, KLS/LogConcave/Regular/Basic, Analysis/BakryEmery/Tilt/Basic.

Selected supporting theorems: contDiffOn_logLaplace_ball, convexOn_of_hessian_ge, exists_integrable_exp_norm, exists_f_abs_exponential_moment, exists_graph_norm_moment_of_local_moments.

Previous: joint_first_derivative_of_radii · Next: source_mixed_cumulant_entries.

Source excerpt, lines 360–368 · Frozen source 408915f.