Orthogonality of Normalized Sums to Coordinate Observables

This lemma states an orthogonality identity for a normalized sum on a finite product probability space.

Let $E$ be a measurable space, $\mu$ a probability measure on $E$, and $f,g:E\to\mathbb R$. Assume:

1. $f,g\in L^2(\mu)$, in the sense of MemLp.
2. $\int f\,d\mu=\int g\,d\mu=0$.
3. $\int fg\,d\mu=0$.

For every natural number $N>0$ and every $i\in\operatorname{Fin}N$, put $\nu=\mu^{\otimes N}$ (Measure.pi) and $F_N(x)=N^{-1/2}\sum_{k\in\operatorname{Fin}N}f(x_k)$. Then

The statement supplies both integrability and vanishing of the mixed moment for independent copies.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability. Shown in its original module context. Proof omitted.

theorem integral_normalizedSum_mul_comp_eval_pi
    (μ : Measure E) [IsProbabilityMeasure μ] (f g : E → ℝ)
    (hf2 : MemLp f 2 μ) (hg2 : MemLp g 2 μ)
    (hf0 : ∫ x, f x ∂μ = 0) (hg0 : ∫ x, g x ∂μ = 0)
    (hfg0 : ∫ x, f x * g x ∂μ = 0) (N : ℕ) (hN : 0 < N) (i : Fin N) :
    Integrable (fun x : Fin N → E => ((∑ k, f (x k)) / Real.sqrt N) * g (x i))
      (Measure.pi (fun _ : Fin N => μ)) ∧
      (∫ x : Fin N → E, ((∑ k, f (x k)) / Real.sqrt N) * g (x i)
        ∂(Measure.pi (fun _ : Fin N => μ))) = 0

Module navigation

Module: Probability/Product.

Supporting theorems: integral_mul_comp_eval_pi.

Previous: integral_mul_comp_eval_pi · Next: prod_add_moments.

Source excerpt, lines 195–203 · Frozen source 408915f.