ASTIS mathematical exposition

Integrate a test function through a pushforward measure

AutoSamplingTheory.lawMapIntegral · theorem · Teaching coverage

Statement

Let P be any measure on measurable Ω and let X:Ω→E be P-almost-everywhere measurable. If B is a real normed vector space and φ:E→B is almost-everywhere strongly measurable under X#P, then the integral of φ against X#P equals the integral of φ∘X against P. No integrability or completeness assumption is imposed by this equality.

\[\int_E\varphi(x)\,d(X_\#P)(x)=\int_\Omega\varphi(X(\omega))\,dP(\omega).\]

All objects and hypotheses

Ω and E are arbitrary measurable spaces; P is any measure on Ω, with no finiteness or probability hypothesis.
B has NormedAddCommGroup and NormedSpace ℝ structures; completeness is not assumed.
X:Ω→E is AEMeasurable under P; φ:E→B is AEStronglyMeasurable under X#P.

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\]

Mathematical proof

1. Use the pushforward integration identity

The imported change-of-variables theorem needs the map's a.e. measurability and the test's a.e. strong measurability under its image measure; the supplied assumptions match precisely.

\[\int \varphi\,d(X_\#P)=\int\varphi\circ X\,dP.\]

Corresponding Lean step

integral_map hX hφ

Lean statement · lawMapIntegral

The vector-space assumptions tell Lean how to form the Bochner integral. The two measurability hypotheses concern different domains and measures.

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 lawMapIntegral {Ω E B : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [NormedAddCommGroup B] [NormedSpace ℝ B]
    {P : Measure Ω} {X : Ω → E} {φ : E → B}
    (hX : AEMeasurable X P)
    (hφ : AEStronglyMeasurable φ (Measure.map X P)) :
    (∫ x, φ x ∂Measure.map X P) = ∫ ω, φ (X ω) ∂P

Exact module and namespace context

Lean proof · lawMapIntegral

A single rewrite replaces integration under the image measure by integration of the composed test. No differentiation or integrability proof occurs.

theorem lawMapIntegral {Ω E B : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [NormedAddCommGroup B] [NormedSpace ℝ B]
    {P : Measure Ω} {X : Ω → E} {φ : E → B}
    (hX : AEMeasurable X P)
    (hφ : AEStronglyMeasurable φ (Measure.map X P)) :
    (∫ x, φ x ∂Measure.map X P) = ∫ ω, φ (X ω) ∂P := by
  rw [integral_map hX hφ]

/-- Transport a supplied sample-space derivative to the corresponding
pushforward-law weak-test integral.

The analytic derivative is still an explicit hypothesis.  This lemma only
packages the `Measure.map` integral rewrite needed before applying a future
EM generator/Fokker--Planck theorem.
-/

Exact module and namespace context

Scope and omitted-condition boundaries

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.
∫ 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.
This is a bookkeeping equality, not time differentiability, a generator identity or a Fokker–Planck equation.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.integral_map

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.
MeasureTheory.integral_map — Directly inspected pinned Mathlib theorem/API. Reuse is distinguished from a new ASTIS proof.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.