Samplinglib mathematical lesson

The conditional integral is integrable under the conditioning law

AutoSamplingTheory.condDistribIntegralMapIntegrable · 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 integrable under the joint image measure λ, then C is integrable under m. No a.e. measurability assumption on X is required by this law-space adapter.

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

Lean statement · condDistribIntegralMapIntegrable

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

Exact module and namespace context

Proof roadmap

1Reuse integrability of the conditional average
For an integrable joint integrand, the imported conditional-integral theorem combines a.e. strong measurability with integrability of the norm of the conditional average. The relevant norm bound is controlled by conditional integration of ‖f‖.

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 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. Reuse integrability of the conditional average

For an integrable joint integrand, the imported conditional-integral theorem combines a.e. strong measurability with integrability of the norm of the conditional average. The relevant norm bound is controlled by conditional integration of ‖f‖.

\[f\in L^1(\lambda)\Longrightarrow C\in L^1(m),\qquad\|C(x)\|\le\int\|f(x,y)\|\,dq(x)(y).\]

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 · condDistribIntegralMapIntegrable

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

Download module (.lean)

theorem condDistribIntegralMapIntegrable {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F}
    (hY : AEMeasurable Y μ)
    (hf : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable
      (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.Integrable.integral_condDistrib_map

Mathematical sources

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