Transfer a chosen conditional integral version between equal kernels
AutoSamplingTheory.condDistribIntegralSampleAeEqOfCondExpKernelMap · theorem · Teaching coverage
Mathematical 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.
Lean statement · condDistribIntegralSampleAeEqOfCondExpKernelMap
The theorem consumes a measure-valued equality and a selected field version. It does not construct either of those hypotheses.
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.
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)Proof roadmap
- 1Intersect the two full-measure events
Outside one null set both the measure equality and the field equality hold at the same ω.
- 2Substitute the equal measure, then the field value
An integral depends on its measure argument. Equal measures give equal totalized integrals, after which the supplied field identity closes the equality.
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).
- Ω 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
1. Intersect the two full-measure events
Outside one null set both the measure equality and the field equality hold at the same ω.
Corresponding Lean step
filter_upwards [hkernel,hfield]
2. Substitute the equal measure, then the field value
An integral depends on its measure argument. Equal measures give equal totalized integrals, after which the supplied field identity closes the equality.
Corresponding Lean step
rw [hka,hfa]
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · condDistribIntegralSampleAeEqOfCondExpKernelMap
A finite intersection combines the a.e. assumptions, and two substitutions identify the integral. No conditional expectation or measurability theorem is re-proved.
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.
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]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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
- Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.