Samplinglib mathematical lesson

The conditional integral is almost-everywhere strongly measurable under the conditioning law

AutoSamplingTheory.condDistribIntegralMapAEStronglyMeasurable · theorem · Teaching coverage

Read this first

Mathematical statement

In the finite-measure conditional-distribution setting and notation below, assume Y is μ-a.e. measurable. If f is almost-everywhere strongly measurable under the joint image measure λ, then C is almost-everywhere strongly measurable under m. No a.e. measurability assumption on X is required by this law-space adapter.

\[f\in\operatorname{AESM}(\lambda)\Longrightarrow C\in\operatorname{AESM}(m).\]

Lean statement · condDistribIntegralMapAEStronglyMeasurable

The measure attached to the conclusion is the conditioning image measure m. The hypothesis concerns the joint measure λ, not every individual conditional 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 condDistribIntegralMapAEStronglyMeasurable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hY : AEMeasurable Y μ)
    (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) :
    AEStronglyMeasurable
      (fun x => ∫ y, f (x, y) ∂ProbabilityTheory.condDistrib Y X μ x)
      (μ.map X)

Exact module and namespace context

Proof roadmap

1Apply the canonical conditional-integral measurability result
Mathlib identifies the first marginal of the joint image measure using the a.e. measurability of Y, and its disintegration backend supplies a strongly measurable version of the conditional integral under that marginal.

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).
Y is μ-a.e. measurable.
f is almost-everywhere strongly measurable 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. Apply the canonical conditional-integral measurability result

Mathlib identifies the first marginal of the joint image measure using the a.e. measurability of Y, and its disintegration backend supplies a strongly measurable version of the conditional integral under that marginal.

\[f\text{ is }\lambda\text{-a.e. strongly measurable}\Longrightarrow C\text{ is }m\text{-a.e. strongly measurable}.\]

Corresponding Lean step

hf.integral_condDistrib_map hY

Lean verification

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

Lean proof · condDistribIntegralMapAEStronglyMeasurable

This is direct reuse of Mathlib's law-space conditional-integral measurability theorem. The displayed argument explains that theorem's role; ASTIS adds no independent disintegration proof.

Download module (.lean)

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

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.
X need not be a.e. measurable in this exact signature; without it, the displayed image measures retain Mathlib's totalized-map semantics.
No specified SALD component version, path law, or weak PDE is constructed.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
MeasureTheory.AEStronglyMeasurable.integral_condDistrib_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.