Moments Of A Sum Under A Product Measure

Proved

FunctionalInequalities.Probability.prod_add_moments_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement computes the moments of a sum of two independent centered variables.

Let $\mu$ and $\nu$ be probability measures on measurable spaces $A$ and $B$ . Let $X:A\to\mathbb R$ and $Y:B\to\mathbb R$ belong to $L^2$ and satisfy

\int_A X\,d\mu=0,\qquad \int_B Y\,d\nu=0.

Then $(a,b)\mapsto X(a)+Y(b)$ belongs to $L^2(\mu\otimes\nu)$ , has mean zero, and satisfies

\int_{A\times B}(X(a)+Y(b))^2\,d(\mu\otimes\nu) =\int_A X^2\,d\mu+\int_B Y^2\,d\nu.

The result is a reusable second-moment identity for independent sums.

Original Lean declaration header

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

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

Module navigation

Module: Probability/Product.

Previous: integral_normalizedSum_mul_comp_eval_pi · Next: integral_prod_add_mul_eq_zero.

Source excerpt, lines 245–252 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Product

open MeasureTheory ProbabilityTheory Filter
variable {A B : Type*}
variable [MeasurableSpace A] [MeasurableSpace B]

Formal statement


theorem FunctionalInequalities.Probability.prod_add_moments_readable
    (μ : Measure A) (ν : Measure B) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (X : A → ℝ) (Y : B → ℝ) (hX2 : MemLp X 2 μ) (hY2 : MemLp Y 2 ν)
    (hX0 : ∫ x, X x ∂μ = 0) (hY0 : ∫ y, Y y ∂ν = 0) :
    MemLp (fun p : A × B => X p.1 + Y p.2) 2 (μ.prod ν) ∧
      (∫ p : A × B, X p.1 + Y p.2 ∂(μ.prod ν)) = 0 ∧
      (∫ p : A × B, (X p.1 + Y p.2) ^ 2 ∂(μ.prod ν)) =
        (∫ x, X x ^ 2 ∂μ) + (∫ y, Y y ^ 2 ∂ν) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Product.lean#L243-L265 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Product`, declaration `FunctionalInequalities.Probability.prod_add_moments`; the repository is private at upload time).

View graph