Samplinglib mathematical lesson

Match the conditional distribution and mapped conditional-expectation kernel

AutoSamplingTheory.condDistribAeEqCondExpKernelMap · theorem · Teaching coverage

Read this first

Mathematical statement

Let Ω and γ be Standard Borel measurable spaces, with γ nonempty; let β be any measurable space and μ any finite measure on Ω. For measurable X:Ω→β and Y:Ω→γ and a fixed measurable set S⊆γ, the selected conditional probability of Y∈S given X, evaluated at X(ω), agrees μ-almost everywhere with the conditional-expectation kernel for σ(X), pushed forward by Y and evaluated on S.

\[q(X\omega,S)=\bigl(Y_\#\,\operatorname{condExpKernel}(\mu,\sigma(X))(\omega)\bigr)(S)\quad\mu\text{-a.e.},\qquad \sigma(X)=\mathcal M_\beta\operatorname{.comap}X.\]

Lean statement · condDistribAeEqCondExpKernelMap

The conclusion is equality of two scalar event probabilities for one fixed measurable S. The order of parameter names in the imported theorem is opposite to this adapter's chosen names.

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 condDistribAeEqCondExpKernelMap {Ω β γ : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [StandardBorelSpace Ω] [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    (hX : Measurable X) (hY : Measurable Y) {s : Set γ}
    (hs : MeasurableSet s) :
    (fun a => ProbabilityTheory.condDistrib Y X μ (X a) s) =ᵐ[μ]
      fun a =>
        (ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a s

Exact module and namespace context

Proof roadmap

1Use the conditional-kernel comparison theorem
Mathlib already compares the conditional distribution of a sampled variable with the image of the sample-space conditional-expectation kernel. Its convention lists the sampled variable first and the conditioning variable second.
2Match the roles without swapping the meaning
Set the imported theorem's sampled variable to Y and its conditioning variable to X. Their measurability and S's measurability are exactly the required inputs.

Full assumptions and notation

All objects and hypotheses

Ω, β, γ have measurable-space structures; Ω and γ are Standard Borel, and γ is nonempty. No Standard Borel assumption on β or Nonempty Ω is required.
μ is finite; X:Ω→β and Y:Ω→γ are measurable; S⊆γ is measurable.

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.}\]
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. Use the conditional-kernel comparison theorem

Mathlib already compares the conditional distribution of a sampled variable with the image of the sample-space conditional-expectation kernel. Its convention lists the sampled variable first and the conditioning variable second.

\[\operatorname{condDistrib}(V\mid U;\mu)(U\omega,S)=(V_\#Q_{\sigma(U)}(\omega))(S)\quad\mu\text{-a.e.}\]

Corresponding Lean step

ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map

2. Match the roles without swapping the meaning

Set the imported theorem's sampled variable to Y and its conditioning variable to X. Their measurability and S's measurability are exactly the required inputs.

\[V=Y,\quad U=X,\quad q(X\omega,S)=(Y_\#Q_{\sigma(X)}(\omega))(S)\quad\mu\text{-a.e.}\]

Corresponding Lean step

(X := Y) (Y := X) hY hX hs

Lean verification

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

Lean proof · condDistribAeEqCondExpKernelMap

The proof directly specializes the imported orientation theorem. It does not prove equality of measures on one common full-measure set for all S.

Download module (.lean)

theorem condDistribAeEqCondExpKernelMap {Ω β γ : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [StandardBorelSpace Ω] [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    (hX : Measurable X) (hY : Measurable Y) {s : Set γ}
    (hs : MeasurableSet s) :
    (fun a => ProbabilityTheory.condDistrib Y X μ (X a) s) =ᵐ[μ]
      fun a =>
        (ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a s := by
  exact ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map
    (μ := μ) (X := Y) (Y := X) hY hX hs

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.
The exceptional set may depend on the fixed event S; do not upgrade this declaration alone to measure-valued a.e. kernel equality.
No weak Fokker–Planck equation or KL differentiability result.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map

Mathematical sources

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