Samplinglib mathematical lesson

Integrating the conditional average recovers the joint integral

AutoSamplingTheory.condDistribIntegralMapIntegral · theorem · Teaching coverage

Read this first

Mathematical statement

In the finite-measure conditional setting below, assume X and Y are μ-a.e. measurable and f is integrable under their joint image measure λ. Then integrating the conditional integral C(x) against the conditioning law m=X#μ equals integrating f(Xω,Yω) against μ. This is finite-measure disintegration, without probability normalization.

\[\int_\beta\left(\int_\gamma f(x,y)\,dq(x)(y)\right)\,dm(x)=\int_\Omega f(X\omega,Y\omega)\,d\mu(\omega).\]

Lean statement · condDistribIntegralMapIntegral

The integrability assumption belongs to the joint measure. The conclusion averages over the conditioning law and does not demand integrability on every null fiber.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem condDistribIntegralMapIntegral {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    (∫ x, ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x
        ∂μ.map X) =
      ∫ a, f (X a, Y a) ∂μ

Exact module and namespace context

Proof roadmap

1Recover the joint image measure by disintegration
The general disintegration theorem with sampled variable Y gives λ=m⊗ₘq. The marginal is finite and q is Markov, providing the s-finiteness needed by the composition-product integral API.
2Transfer integrability to the composition-product
Because the two joint measures are equal, the supplied integrability of f under λ applies to m⊗ₘq.
3Use the iterated-integral identity
The composition-product integral theorem identifies the outer conditional average with integration over the reconstructed joint measure.
4Return to the original sample space
Replace the composition-product by the joint image measure and use the measurable-pair pushforward integration formula.

Full assumptions and notation

All objects and hypotheses

Ω, β and γ are measurable spaces; γ is Standard Borel and nonempty.
μ is a finite measure on Ω, not necessarily a probability; X:Ω→β and Y:Ω→γ are functions.
F is a real normed vector space (NormedAddCommGroup and NormedSpace ℝ); no CompleteSpace assumption is added. The integrand f:β×γ→F is as specified below.
Notation: λ=(ω↦(Xω,Yω))#μ, m=X#μ, q(x)=condDistrib(Y|X;μ)(x), and C(x)=∫f(x,y)dq(x)(y).
X and Y are μ-a.e. measurable, and f is λ-integrable.

Notation and interpretation

Pushforward law: P is an arbitrary measure unless explicitly declared finite or a probability. The word law here abbreviates a pushforward measure; probability-language interpretations require normalization separately. Mathlib totalizes map to zero when X is not a.e. measurable; unqualified map-congruence and some law-space adapters intentionally retain that generality.
\[(X_\#\mu)(A)=\mu(X^{-1}A)\quad\text{when the measurable pushforward interpretation applies}\]
A.e. and strong measurability: A.e. means outside a μ-null set. AEMeasurable means equality a.e. to a measurable map; AEStronglyMeasurable (abbreviated AESM) means equality a.e. to a strongly measurable function, which is approximable by simple functions.
\[f=g\quad\mu\text{-a.e.}\]
Integrability and Bochner integrals: L¹ in the teaching formulas means Integrable, not a newly defined quotient-space element. ∫ denotes Mathlib's totalized Bochner integral: it is zero for nonintegrable functions, and also for a codomain lacking completeness. Do not infer integrability or a genuine finite expectation from an unqualified integral equality. Real-valued integrals have a complete codomain; missing integrability still matters.
\[f\in L^1(\mu)\quad\Longleftrightarrow\quad f\text{ is a.e. strongly measurable and }\int^{\!-}\|f\|\,d\mu<\infty\]
Conditional integral notation: The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted. Finite non-probability measures are reconstructed with their original total mass; any version changes on marginal-null inputs must retain a measurable kernel.
\[\lambda=(X,Y)_\#\mu,\quad m=X_\#\mu,\quad q(x)=\operatorname{condDistrib}(Y\mid X;\mu)(x),\quad C(x)=\int f(x,y)\,dq(x)(y)\]

Mathematical proof

1. Recover the joint image measure by disintegration

The general disintegration theorem with sampled variable Y gives λ=m⊗ₘq. The marginal is finite and q is Markov, providing the s-finiteness needed by the composition-product integral API.

\[m\otimes_m q=\lambda.\]

Corresponding Lean step

ProbabilityTheory.compProd_map_condDistrib hY; hcomp

2. Transfer integrability to the composition-product

Because the two joint measures are equal, the supplied integrability of f under λ applies to m⊗ₘq.

\[f\in L^1(\lambda)\Longrightarrow f\in L^1(m\otimes_m q).\]

Corresponding Lean step

hfComp; rw [hcomp]; exact hf

3. Use the iterated-integral identity

The composition-product integral theorem identifies the outer conditional average with integration over the reconstructed joint measure.

\[\int\!\int f(x,y)\,dq(x)(y)\,dm(x)=\int f\,d(m\otimes_m q).\]

Corresponding Lean step

(Measure.integral_compProd hfComp).symm

4. Return to the original sample space

Replace the composition-product by the joint image measure and use the measurable-pair pushforward integration formula.

\[\int f\,d\lambda=\int f(X\omega,Y\omega)\,d\mu.\]

Corresponding Lean step

rw [hcomp]; integral_map (hX.prodMk hY) hf.1

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · condDistribIntegralMapIntegral

The proof names the disintegration equality, transports the integrability hypothesis, reverses the iterated-integral theorem, and changes variables through the paired map.

Download module (.lean)

theorem condDistribIntegralMapIntegral {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    (∫ x, ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x
        ∂μ.map X) =
      ∫ a, f (X a, Y a) ∂μ := by
  have hcomp := ProbabilityTheory.compProd_map_condDistrib
    (μ := μ) (X := X) (Y := Y) (mβ := inferInstance) hY
  have hfComp :
      Integrable f ((μ.map X) ⊗ₘ ProbabilityTheory.condDistrib Y X μ) := by
    rw [hcomp]
    exact hf
  calc
    (∫ x, ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x
        ∂μ.map X)
        = ∫ z, f z ∂((μ.map X) ⊗ₘ
            ProbabilityTheory.condDistrib Y X μ) := by
          exact (Measure.integral_compProd
            (μ := μ.map X) (κ := ProbabilityTheory.condDistrib Y X μ)
            hfComp).symm
    _ = ∫ a, f (X a, Y a) ∂μ := by
          rw [hcomp]
          rw [integral_map (hX.prodMk hY) hf.1]

Exact module and namespace context

Scope and omitted-condition boundaries

The selected conditional distribution is a probability kernel, characterized as a conditional law only almost everywhere under the conditioning marginal. No pointwise choice, simultaneous equality on all events from a single-event a.e. theorem, or null-fiber support is asserted.
∫ denotes Mathlib's totalized Bochner integral: it is zero for nonintegrable functions, and also for a codomain lacking completeness. Do not infer integrability or a genuine finite expectation from an unqualified integral equality. Real-valued integrals have a complete codomain; missing integrability still matters.
For probability μ this is a two-stage expectation identity. For general finite μ, q(x) has mass one but the outer measure m has total mass μ(Ω); the reconstruction preserves that mass.
No integration by parts, admissible log-ratio test or Fokker–Planck theorem.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.compProd_map_condDistrib
MeasureTheory.Measure.integral_compProd
MeasureTheory.integral_map
AEMeasurable.prodMk

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
ProbabilityTheory.compProd_map_condDistrib — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
MeasureTheory.Measure.integral_compProd — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.
MeasureTheory.integral_map — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.