Samplinglib mathematical lesson

Disintegration written with a named conditioning law

AutoSamplingTheory.condDistribIntegralNamedLawIntegral · theorem · Teaching coverage

Read this first

Mathematical statement

In the finite-measure conditional setting below, let ρ̂ be a measure on β with ρ̂=X#μ. Assume Y is μ-a.e. measurable and X is μ-a.e. measurable, and f is integrable under λ. Then the averaged conditional integral equals the joint sample integral. This only replaces the mapped measure by an equal named measure.

\[\widehat\rho=m\Longrightarrow\int C\,d\widehat\rho=\int f(X\omega,Y\omega)\,d\mu.\]

Lean statement · condDistribIntegralNamedLawIntegral

The named measure is not inferred from notation; its equality to X#μ is an explicit premise. The remaining assumptions are exactly those of the reused theorem.

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 condDistribIntegralNamedLawIntegral {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F}
    (hhatRho : hatRho = μ.map X)
    (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
        ∂hatRho) =
      ∫ a, f (X a, Y a) ∂μ

Exact module and namespace context

Proof roadmap

1Replace the named measure by the image law
Use the supplied equality exactly where the measure occurs in the conclusion.
2Reuse the canonical law-space theorem
After substitution, the goal is the existing disintegration or regularity theorem with unchanged hypotheses.

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).
ρ̂ is a measure on β and hhatRho gives ρ̂=X#μ.
Y is μ-a.e. measurable.
X is μ-a.e. measurable.
f is integrable under λ.

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. Replace the named measure by the image law

Use the supplied equality exactly where the measure occurs in the conclusion.

\[\widehat\rho=m=X_\#\mu.\]

Corresponding Lean step

rw [hhatRho]

2. Reuse the canonical law-space theorem

After substitution, the goal is the existing disintegration or regularity theorem with unchanged hypotheses.

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

Corresponding Lean step

exact condDistribIntegralMapIntegral ...

Lean verification

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

Lean proof · condDistribIntegralNamedLawIntegral

The proof consists of measure substitution followed by the existing canonical result. The named-law wrapper adds no conditional-law construction or analytic hypothesis.

Download module (.lean)

theorem condDistribIntegralNamedLawIntegral {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {hatRho : Measure β}
    {X : Ω → β} {Y : Ω → γ} {f : β × γ → F}
    (hhatRho : hatRho = μ.map X)
    (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
        ∂hatRho) =
      ∫ a, f (X a, Y a) ∂μ := by
  rw [hhatRho]
  exact condDistribIntegralMapIntegral hX hY hf

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.
Reuse wrapper, not a separate proof of disintegration.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.condDistribIntegralMapIntegral

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
AutoSamplingTheory.condDistribIntegralMapIntegral — Existing root ASTIS dependency; use its own adjacent teaching unit.

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