Second Moments of the Suspension Joint Law With Explicit Laplace Data

This lemma states finite second moment, zero mean, and identity covariance for the suspension joint law under explicit Laplace moment hypotheses.

Let $n,N\in\mathbb N$ with $N>0$, and let $\mu$ be a probability measure on $E=\mathbb R^n$ (EuclideanSpace ℝ (Fin n)). Assume:

1. $\operatorname{id}\in L^2(\mu)$, $\int x\,d\mu=0$, and $\int\langle u,x\rangle\langle v,x\rangle\,d\mu=\langle u,v\rangle$ for all $u,v\in E$.
2. $f:E\to\mathbb R$ is measurable and in $L^2(\mu)$, with $\int f\,d\mu=0$, $\int f^2\,d\mu=1$, and $\int\langle u,x\rangle f(x)\,d\mu=0$ for every $u\in E$.
3. $\beta>0$ and $\eta_\beta=$ laplaceMeasure $\beta$ is a probability measure; $s,s^2$ are integrable under it, with integrals $0,2/\beta^2$.

Set $\sigma_\beta=\sqrt{1+2/\beta^2}$ (sigma). Let $\lambda=$ jointLaw $\mu\ f\ \beta\ \sigma_\beta\ N$, the law of $((N^{-1/2}\sum_i f(X_i)+\eta)/\sigma_\beta,X_1,\ldots,X_N)$ under independent copies and independent noise. Its target $H=$ JointSpace $N\ n$ is $\mathbb R^{\operatorname{Option}(\operatorname{Fin}N\times\operatorname{Fin}n)}$. Then

These are the moment data used to establish isotropy of the joint law; log-concavity is not assumed here.

Original Lean declaration header

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

theorem jointLaw_moments_of_laplace {n N : ℕ} (hN : 0 < N)
    (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) (hμ0 : ∫ x, x ∂μ = 0)
    (hμcov : ∀ u v : EuclideanSpace ℝ (Fin n), ∫ x, ⟪u, x⟫ * ⟪v, x⟫ ∂μ = ⟪u, v⟫)
    {f : EuclideanSpace ℝ (Fin n) → ℝ} (hf : Measurable f) (hf2 : MemLp f 2 μ)
    (hf0 : ∫ x, f x ∂μ = 0) (hf1 : ∫ x, f x ^ 2 ∂μ = 1) (hfx : ∀ u, ∫ x, ⟪u, x⟫ * f x ∂μ = 0)
    {β : ℝ} (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 id 2 (jointLaw μ f β (sigma β) N) ∧ ∫ p, p ∂(jointLaw μ f β (sigma β) N) = 0 ∧
      ∀ u v : JointSpace N n, ∫ p, ⟪u, p⟫ * ⟪v, p⟫ ∂(jointLaw μ f β (sigma β) N) = ⟪u, v⟫

Module navigation

Module: KLS/BKL/Suspension/Moments.

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

Supporting theorems: integral_scalar_mul_inner, scalar_moments, integral_mul_comp_eval_pi, euclideanMomentsFromCoordinates.

Previous: euclideanMomentsFromCoordinates.

Source excerpt, lines 243–254 · Frozen source 408915f.