Products Of Coordinates In A Finite Product

Proved

FunctionalInequalities.Probability.integral_mul_comp_eval_pi_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement computes products of coordinate observables under a finite product measure.

Let $\mu$ be a probability measure on $E$ , and let $f,g:E\to\mathbb R$ belong to $L^2(\mu)$ . For any $N\in\mathbb N$ and $i,j\in\operatorname{Fin}N$ , the product $x\mapsto f(x_i)g(x_j)$ is integrable under $\mu^{\otimes N}$ , and

\int f(x_i)g(x_j)\,d\mu^{\otimes N} =\begin{cases} \displaystyle\int f(x)g(x)\,d\mu(x),&i=j,\\[6pt] \displaystyle\left(\int f\,d\mu\right)\left(\int g\,d\mu\right),&i\ne j. \end{cases}

This is the coordinate-product identity underlying covariance and isotropy computations for independent copies.

Formalization Note. The two cases are represented by an if expression on the equality of the finite indices.

Original Lean declaration header

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

theorem integral_mul_comp_eval_pi
    (μ : Measure E) [IsProbabilityMeasure μ] (f g : E → ℝ)
    (hf2 : MemLp f 2 μ) (hg2 : MemLp g 2 μ) (N : ℕ) (i j : Fin N) :
    Integrable (fun x : Fin N → E => f (x i) * g (x j))
      (Measure.pi (fun _ : Fin N => μ)) ∧
      (∫ x : Fin N → E, f (x i) * g (x j) ∂(Measure.pi (fun _ : Fin N => μ))) =
        if i = j then ∫ x, f x * g x ∂μ
          else (∫ x, f x ∂μ) * (∫ x, g x ∂μ)

Module navigation

Module: Probability/Product.

Previous: pi_normalizedSum_moments · Next: integral_normalizedSum_mul_comp_eval_pi.

Source excerpt, lines 151–158 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Product

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

Formal statement


theorem FunctionalInequalities.Probability.integral_mul_comp_eval_pi_readable
    (μ : Measure E) [IsProbabilityMeasure μ] (f g : E → ℝ)
    (hf2 : MemLp f 2 μ) (hg2 : MemLp g 2 μ) (N : ℕ) (i j : Fin N) :
    Integrable (fun x : Fin N → E => f (x i) * g (x j))
      (Measure.pi (fun _ : Fin N => μ)) ∧
      (∫ x : Fin N → E, f (x i) * g (x j) ∂(Measure.pi (fun _ : Fin N => μ))) =
        if i = j then ∫ x, f x * g x ∂μ
          else (∫ x, f x ∂μ) * (∫ x, g x ∂μ) := by sorry

Source

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

View graph