Euclidean Moment Identities From Coordinate Moments

This auxiliary lemma assembles Euclidean moment identities from coordinatewise hypotheses.

Let $A$ be a measurable space, $\nu$ a probability measure on $A$, and $I$ a finite type with decidable equality. Let $Y:A\to\mathbb R^I$ be measurable, with Euclidean target EuclideanSpace ℝ I. Assume:

1. Each coordinate $Y_i$ belongs to $L^2(\nu)$ (MemLp).
2. $\int Y_i\,d\nu=0$ for every $i\in I$.
3. $\int Y_iY_j\,d\nu=\delta_{ij}$ for every $i,j\in I$, where $\delta_{ij}$ is $1$ if $i=j$ and $0$ otherwise.

Then

This provides a finite-dimensional interface between coordinate moments and the bilinear second-moment identity.

Original Lean declaration header

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

private theorem euclideanMomentsFromCoordinates {A I : Type*} [MeasurableSpace A]
    [Fintype I] [DecidableEq I] (ν : Measure A) [IsProbabilityMeasure ν] (Y : A → EuclideanSpace ℝ I)
    (hY : Measurable Y) (h2 : ∀ i, MemLp (fun x => Y x i) 2 ν)
    (h0 : ∀ i, (∫ x, Y x i ∂ν) = 0)
    (hcov : ∀ i j, (∫ x, Y x i * Y x j ∂ν) = if i = j then 1 else 0) :
    MemLp Y 2 ν ∧ (∫ x, Y x ∂ν) = 0 ∧
      ∀ u v : EuclideanSpace ℝ I, (∫ x, ⟪u, Y x⟫ * ⟪v, Y x⟫ ∂ν) = ⟪u, v⟫

Module navigation

Module: KLS/BKL/Suspension/Moments.

Previous: integral_scalar_mul_inner · Next: jointLaw_moments_of_laplace.

Source excerpt, lines 178–184 · Frozen source 408915f.