Moments Of The Suspension Coordinate

This statement computes the moments of the scalar suspension coordinate used in Proposition 7.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 28.

Let $N>0$, let $\mu$ be a probability measure on $\mathbb R^n$, and let $f\in L^2(\mu)$ satisfy

$$\int f\,d\mu=0,\qquad \int f^2\,d\mu=1.$$

Let $\beta>0$, and let $\eta$ have the Laplace measure of parameter $\beta$, with

$$\int\eta\,d\eta=0,\qquad \int\eta^2\,d\eta=\frac{2}{\beta^2}.$$

Assume the stated integrability conditions. For independent copies $x_i$ and $\eta$, define

$$S=\frac{N^{-1/2}\sum_i f(x_i)+\eta}{\sigma_\beta}, \qquad \sigma_\beta=\sqrt{1+2/\beta^2}.$$

Then $S\in L^2$, and under the product of the copy measure and the Laplace measure,

$$\int S=0,\qquad \int S^2=1.$$

This supplies the centered, unit-variance scalar coordinate required for isotropy of the suspension law.

Formalization Note. The declaration treats the Laplace probability instance and its first- and second-moment hypotheses as explicit assumptions.

Original Lean declaration header

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

theorem scalar_moments {n N : ℕ} (hN : 0 < N)
    (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf2 : MemLp f 2 μ)
    (hf0 : ∫ x, f x ∂μ = 0) (hf1 : ∫ x, f x ^ 2 ∂μ = 1)
    {β : ℝ} (hβ : 0 < β) [IsProbabilityMeasure (laplaceMeasure β)]
    (hη1 : Integrable (fun s : ℝ => s) (laplaceMeasure β))
    (hη2 : Integrable (fun s : ℝ => s ^ 2) (laplaceMeasure β))
    (hη0 : ∫ s, s ∂laplaceMeasure β = 0) (hηv : ∫ s, s ^ 2 ∂laplaceMeasure β = 2 / β ^ 2) :
    MemLp (fun q : (Fin N → EuclideanSpace ℝ (Fin n)) × ℝ =>
      (copyStat f N q.1 + q.2) / sigma β) 2
      ((Measure.pi (fun _ : Fin N => μ)).prod (laplaceMeasure β)) ∧
      (∫ q : (Fin N → EuclideanSpace ℝ (Fin n)) × ℝ,
        (copyStat f N q.1 + q.2) / sigma β
        ∂((Measure.pi (fun _ : Fin N => μ)).prod (laplaceMeasure β))) = 0 ∧
      (∫ q : (Fin N → EuclideanSpace ℝ (Fin n)) × ℝ,
        ((copyStat f N q.1 + q.2) / sigma β) ^ 2
        ∂((Measure.pi (fun _ : Fin N => μ)).prod (laplaceMeasure β))) = 1

Module navigation

Module: KLS/BKL/Suspension/Moments.

Definition modules: KLS/BKL/Suspension/Law, Probability/Line/Laplace.

Supporting theorems: pi_normalizedSum_moments, prod_add_moments.

Next: integral_scalar_mul_inner.

Source excerpt, lines 88–104 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Suspension_Moments

open MeasureTheory ProbabilityTheory FunctionalInequalities.Probability
open FunctionalInequalities.Probability.Line

theorem FunctionalInequalities.KLS.LogConcave.Suspension.scalar_moments_readable {n N : ℕ} (hN : 0 < N)
    (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf2 : MemLp f 2 μ)
    (hf0 : ∫ x, f x ∂μ = 0) (hf1 : ∫ x, f x ^ 2 ∂μ = 1)
    {β : ℝ} (hβ : 0 < β) [IsProbabilityMeasure (laplaceMeasure β)]
    (hη1 : Integrable (fun s : ℝ => s) (laplaceMeasure β))
    (hη2 : Integrable (fun s : ℝ => s ^ 2) (laplaceMeasure β))
    (hη0 : ∫ s, s ∂laplaceMeasure β = 0) (hηv : ∫ s, s ^ 2 ∂laplaceMeasure β = 2 / β ^ 2) :
    MemLp (fun q : (Fin N → EuclideanSpace ℝ (Fin n)) × ℝ =>
      (copyStat f N q.1 + q.2) / sigma β) 2
      ((Measure.pi (fun _ : Fin N => μ)).prod (laplaceMeasure β)) ∧
      (∫ q : (Fin N → EuclideanSpace ℝ (Fin n)) × ℝ,
        (copyStat f N q.1 + q.2) / sigma β
        ∂((Measure.pi (fun _ : Fin N => μ)).prod (laplaceMeasure β))) = 0 ∧
      (∫ q : (Fin N → EuclideanSpace ℝ (Fin n)) × ℝ,
        ((copyStat f N q.1 + q.2) / sigma β) ^ 2
        ∂((Measure.pi (fun _ : Fin N => μ)).prod (laplaceMeasure β))) = 1 := by sorry