Prove2Me

Product Measure Variance Decomposition

Proved
FunctionalInequalities.ProductVariance.decomposition_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the law of total variance for a product probability measure.

Let μ\mu and ν\nu be probability measures on measurable spaces EE and FF, and let f:E×F→Rf:E\times F\to\mathbb R belong to L2(μ⊗ν)L^2(\mu\otimes\nu). Then

Var⁡μ⊗ν(f)=∫EVar⁡ν(y↦f(x,y)) dμ(x)+Var⁡μ ⁣(x↦∫Ff(x,y) dν(y)).\operatorname{Var}_{\mu\otimes\nu}(f) =\int_E\operatorname{Var}_{\nu}\bigl(y\mapsto f(x,y)\bigr)\,d\mu(x) +\operatorname{Var}_{\mu}\!\left(x\mapsto\int_F f(x,y)\,d\nu(y)\right).

The explicit MemLp f 2 assumption supplies the iterated integrability needed for the ordinary integral formulation.

Original Lean declaration header

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

theorem decomposition (hf : MemLp f 2 (μ.prod ν)) :
    variance f (μ.prod ν) =
      (∫ x, variance (fun y ↦ f (x, y)) ν ∂μ) +
      variance (fun x ↦ ∫ y, f (x, y) ∂ν) μ

Module navigation

Module: Probability/ProductVariance.

Source excerpt, lines 104–107 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_ProductVariance

open MeasureTheory ProbabilityTheory
variable {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]
  {μ : MeasureTheory.Measure E} {ν : MeasureTheory.Measure F} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν]
  {f : E × F → ℝ}
Formal statement

theorem FunctionalInequalities.ProductVariance.decomposition_readable (hf : MemLp f 2 (μ.prod ν)) :
    variance f (μ.prod ν) =
      (∫ x, variance (fun y ↦ f (x, y)) ν ∂μ) +
      variance (fun x ↦ ∫ y, f (x, y) ∂ν) μ := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/ProductVariance.lean#L101-L124 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.ProductVariance`, declaration `FunctionalInequalities.ProductVariance.decomposition`; the repository is private at upload time).

View graph