Finite Product Factorization Of Lower Integrals

Proved

FunctionalInequalities.Probability.lintegral_pi_prod_fin_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement gives the finite-product factorization of a lower integral.

Let $E$ be a measurable space, let $\mu$ be a sigma-finite measure on $E$ , let $k\in\mathbb N$ , and let $g_i:E\to[0,\infty]$ be measurable for every $i\in\operatorname{Fin}k$ . Then

\int_{E^{\operatorname{Fin}k}}\prod_i g_i(x_i)\,d\bigotimes_i\mu =\prod_i\int_E g_i(x)\,d\mu(x).

This is the finite-coordinate independence identity used in product-measure and suspension moment calculations.

Formalization Note. The integrands and integrals take values in $[0,\infty]$ , represented by ENNReal; the product measure is Measure.pi.

Original Lean declaration header

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

theorem lintegral_pi_prod_fin
    (μ : Measure E) [SigmaFinite μ] (k : ℕ) (g : Fin k → E → ENNReal)
    (hg : ∀ i, Measurable (g i)) :
    (∫⁻ x, ∏ i : Fin k, g i (x i) ∂(Measure.pi fun _ : Fin k => μ)) =
      ∏ i : Fin k, ∫⁻ x, g i x ∂μ

Module navigation

Module: Probability/Product.

Next: pi_normalizedSum_moments.

Source excerpt, lines 27–31 · 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.lintegral_pi_prod_fin_readable
    (μ : Measure E) [SigmaFinite μ] (k : ℕ) (g : Fin k → E → ENNReal)
    (hg : ∀ i, Measurable (g i)) :
    (∫⁻ x, ∏ i : Fin k, g i (x i) ∂(Measure.pi fun _ : Fin k => μ)) =
      ∏ i : Fin k, ∫⁻ x, g i x ∂μ := by sorry

Source

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

View graph