ASTIS mathematical exposition

Almost-everywhere equal variables have the same pushforward

AutoSamplingTheory.lawMapEqOfAEEq · theorem · Teaching coverage

Statement

On measurable spaces Ω and E, let P be any measure and X,Y:Ω→E any functions. If X=Y P-almost everywhere, their pushforward measures are equal. No measurability assumption is present in this totalized-map identity.

\[X=Y\quad P\text{-a.e.}\ \Longrightarrow\ X_\#P=Y_\#P.\]

All objects and hypotheses

Ω and E are arbitrary measurable spaces; P is any measure on Ω, with no finiteness or probability hypothesis.
X,Y are arbitrary functions Ω→E; hXY asserts their P-almost-everywhere equality.

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

Mathematical proof

1. Keep the same equivalence class

An almost-everywhere change of a map does not change its Mathlib pushforward. The imported map-congruence theorem applies directly, including its totalized non-a.e.-measurable case.

\[X_\#P=Y_\#P\quad\text{whenever }X=Y\ P\text{-a.e.}\]

Corresponding Lean step

Measure.map_congr hXY

Lean statement · lawMapEqOfAEEq

The hypothesis compares two functions outside a P-null set; the conclusion compares measures, not sample values at every input.

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 lawMapEqOfAEEq {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X Y : Ω → E}
    (hXY : X =ᵐ[P] Y) :
    Measure.map X P = Measure.map Y P

Exact module and namespace context

Lean proof · lawMapEqOfAEEq

The proof applies the existing pushforward-congruence theorem once. It does not construct a process or establish either variable's measurability.

theorem lawMapEqOfAEEq {Ω E : Type*} [MeasurableSpace Ω] [MeasurableSpace E]
    {P : Measure Ω} {X Y : Ω → E}
    (hXY : X =ᵐ[P] Y) :
    Measure.map X P = Measure.map Y P := by
  exact Measure.map_congr hXY

/-- Integrating a test against a pushforward law is the same as integrating
the composed test on the original probability space.

This is the weak-test bookkeeping used before differentiating EM
interpolation laws.  It does not prove any time differentiability, generator
identity, conditional law, density, or Fokker--Planck equation.
-/

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.
Measure.map is totalized: without AEMeasurable assumptions, this is not a claim that the expression is the usual nondegenerate distribution of an arbitrary nonmeasurable random variable.
No pointwise equality, process construction, conditional drift, or density theorem.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Measure.map_congr

Mathematical sources

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