Orthogonality After Adding an Independent Centered Observable

This lemma gives a vanishing mixed moment on a binary product probability space.

Let $A,B$ be measurable spaces with probability measures $\mu,\nu$, respectively. Let $X,Z:A\to\mathbb R$ and $Y:B\to\mathbb R$. Assume:

1. $X,Z\in L^2(\mu)$ and $Y\in L^2(\nu)$ (MemLp).
2. $\int XZ\,d\mu=0$.
3. $\int Y\,d\nu=0$.

For the product measure $\mu\otimes\nu$ (Measure.prod),

This is a reusable mixed-moment identity; neither $X$ nor $Z$ is required to be centered.

Original Lean declaration header

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

theorem integral_prod_add_mul_eq_zero
    (μ : Measure A) (ν : Measure B) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (X Z : A → ℝ) (Y : B → ℝ)
    (hX2 : MemLp X 2 μ) (hZ2 : MemLp Z 2 μ) (hY2 : MemLp Y 2 ν)
    (hXZ0 : ∫ x, X x * Z x ∂μ = 0) (hY0 : ∫ y, Y y ∂ν = 0) :
    Integrable (fun p : A × B => (X p.1 + Y p.2) * Z p.1) (μ.prod ν) ∧
      (∫ p : A × B, (X p.1 + Y p.2) * Z p.1 ∂(μ.prod ν)) = 0

Module navigation

Module: Probability/Product.

Previous: prod_add_moments.

Source excerpt, lines 268–274 · Frozen source 408915f.