Match the conditional distribution and mapped conditional-expectation kernel

AutoSamplingTheory.condDistribAeEqCondExpKernelMap · theorem · Teaching coverage

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.

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

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

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

/-- Sample-space component-version bridge from `condExpKernel.map` to
`condDistrib`.

For the SALD `condC` field, this isolates the remaining Mathlib-facing
boundary after `condDistrib` and `condExpKernel.map` have been aligned as
measure-valued kernels almost everywhere.  It turns a selected
`condExpKernel.map` version of the component field into the displayed
`condDistrib` integral equality after composing with `hat X_s`.  The theorem
does not prove the measure-valued kernel equality or choose the component
version; those remain the smaller conditional-kernel obligations.
-/

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.