Vanishing Cross Moments of the Suspension Scalar and Copies

This lemma states that the suspension scalar has zero mixed moment with every linear observable of each copy.

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)$ and $\int x\,d\mu(x)=0$.
2. $f:E\to\mathbb R$ belongs to $L^2(\mu)$, $\int f\,d\mu=0$, $\int f^2\,d\mu=1$, and $\int\langle u,x\rangle f(x)\,d\mu(x)=0$ for every $u\in E$.
3. $\beta>0$, and $\eta_\beta=$ laplaceMeasure $\beta$ is a probability measure. Both $s$ and $s^2$ are integrable under $\eta_\beta$, with integrals $0$ and $2/\beta^2$, respectively.

Put $F_N(x)=\sum_k f(x_k)/\sqrt N$ (copyStat), $\sigma_\beta=\sqrt{1+2/\beta^2}$ (sigma), $S(x,s)=(F_N(x)+s)/\sigma_\beta$, and $P=\mu^{\otimes N}\otimes\eta_\beta$. For every $i\in\operatorname{Fin}N$ and $u\in E$,

This supplies cross-moment data for the suspension. No identity-covariance or log-concavity assumption on $\mu$ is imposed.

Original Lean declaration header

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

theorem integral_scalar_mul_inner {n N : ℕ} (hN : 0 < N)
    (μ : Measure (EuclideanSpace ℝ (Fin n))) [IsProbabilityMeasure μ]
    (hμ2 : MemLp id 2 μ) (hμ0 : ∫ x, x ∂μ = 0)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (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)
    (i : Fin N) (u : EuclideanSpace ℝ (Fin n)) :
    Integrable (fun q : (Fin N → EuclideanSpace ℝ (Fin n)) × ℝ =>
      ((copyStat f N q.1 + q.2) / sigma β) * ⟪u, q.1 i⟫)
      ((Measure.pi (fun _ : Fin N => μ)).prod (laplaceMeasure β)) ∧
      (∫ q : (Fin N → EuclideanSpace ℝ (Fin n)) × ℝ,
        ((copyStat f N q.1 + q.2) / sigma β) * ⟪u, q.1 i⟫
        ∂((Measure.pi (fun _ : Fin N => μ)).prod (laplaceMeasure β))) = 0

Module navigation

Module: KLS/BKL/Suspension/Moments.

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

Supporting theorems: scalar_moments, integral_normalizedSum_mul_comp_eval_pi, integral_prod_add_mul_eq_zero, pi_normalizedSum_moments.

Previous: scalar_moments · Next: euclideanMomentsFromCoordinates.

Source excerpt, lines 127–143 · Frozen source 408915f.