Transfer a chosen conditional integral version between equal kernels

AutoSamplingTheory.condDistribIntegralSampleAeEqOfCondExpKernelMap · theorem · Teaching coverage

Statement

Use the finite-measure conditional-kernel setting with Ω additionally Standard Borel. Suppose q(Xω) and the Y-image of the conditional-expectation kernel for σ(X) are equal as measures μ-a.e. Suppose integrating y↦f(Xω,y) against the latter measure gives a chosen field v(Xω) μ-a.e. Then integrating against q(Xω) also gives v(Xω) μ-a.e. The two a.e. identities are assumptions.

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 also Standard Borel; v:β→F is a chosen field; R(ω)=(condExpKernel μ σ(X)).map Y (ω).
• hkernel gives equality q(Xω)=R(ω) as measures μ-a.e.; this is stronger than a separate eventwise statement with event-dependent null sets.
• hfield gives the stated integral equality to v(Xω) μ-a.e. No X/Y measurability or f integrability is separately assumed by this substitution theorem.

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

theorem condDistribIntegralSampleAeEqOfCondExpKernelMap {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace Ω] [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F} {field : β → F}
    (hkernel :
      (fun a => ProbabilityTheory.condDistrib Y X μ (X a)) =ᵐ[μ]
        fun a =>
          (ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a)
    (hfield :
      (fun a => ∫ y, f (X a, y)
          ∂(ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a) =ᵐ[μ]
        fun a => field (X a)) :
    (fun a => ∫ y, f (X a, y)
        ∂ProbabilityTheory.condDistrib Y X μ (X a)) =ᵐ[μ]
      fun a => field (X a)

theorem condDistribIntegralSampleAeEqOfCondExpKernelMap {Ω β γ F : Type*}
    [MeasurableSpace Ω] [MeasurableSpace β] [MeasurableSpace γ]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    [StandardBorelSpace Ω] [StandardBorelSpace γ] [Nonempty γ]
    {μ : Measure Ω} [IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ}
    {f : β × γ → F} {field : β → F}
    (hkernel :
      (fun a => ProbabilityTheory.condDistrib Y X μ (X a)) =ᵐ[μ]
        fun a =>
          (ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a)
    (hfield :
      (fun a => ∫ y, f (X a, y)
          ∂(ProbabilityTheory.condExpKernel μ
            ((inferInstance : MeasurableSpace β).comap X)).map Y a) =ᵐ[μ]
        fun a => field (X a)) :
    (fun a => ∫ y, f (X a, y)
        ∂ProbabilityTheory.condDistrib Y X μ (X a)) =ᵐ[μ]
      fun a => field (X a) := by
  filter_upwards [hkernel, hfield] with a hka hfa
  rw [hka, hfa]

/-- Strong measurability of a vector-valued conditional integral against
`condDistrib`.

This packages the Mathlib theorem in the orientation used by the SALD
component fields: conditioning variable `X`, sampled variable `Y`, and an
integrand on `(X,Y)`.  It does not prove the EM interpolation law or any weak
Fokker--Planck identity.
-/

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.
• No regularity of the chosen field follows from this substitution alone.