ASTIS mathematical exposition

Componentwise a.e. equality preserves the joint image law

AutoSamplingTheory.lawMapProdEqOfAEEq · theorem · Teaching coverage

Statement

Let Ω,E,F be measurable spaces, P any measure, X,X′:Ω→E and Y,Y′:Ω→F any functions. If X=X′ P-a.e. and Y=Y′ P-a.e., then the image measures of the paired variables (X,Y) and (X′,Y′) are equal. No separate measurability is assumed.

\[X=X'\ P\text{-a.e.},\quad Y=Y'\ P\text{-a.e.}\ \Longrightarrow\ (X,Y)_\#P=(X',Y')_\#P.\]

All objects and hypotheses

Ω,E,F are measurable spaces; P is any measure on Ω.
X,X′:Ω→E and Y,Y′:Ω→F; the two component equalities hold P-almost everywhere.

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. Combine the two full-measure sets

A finite intersection of a.e. events is again a.e.; outside the union of the two exceptional null sets, both coordinate equalities hold.

\[(X(\omega),Y(\omega))=(X'(\omega),Y'(\omega))\quad P\text{-a.e.}\]

Corresponding Lean step

filter_upwards [hX,hY]; simp [hx,hy]

2. Apply map congruence

Pushforwards do not change under a.e.-equal maps, so the paired image measures agree.

\[(X,Y)_\#P=(X',Y')_\#P.\]

Corresponding Lean step

Measure.map_congr

Lean statement · lawMapProdEqOfAEEq

There are two a.e. equalities but only one underlying measure. This permits combining them into a joint equality on the same sample space.

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 lawMapProdEqOfAEEq {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X X' : Ω → E} {Y Y' : Ω → F}
    (hX : X =ᵐ[P] X') (hY : Y =ᵐ[P] Y') :
    Measure.map (fun ω => (X ω, Y ω)) P =
      Measure.map (fun ω => (X' ω, Y' ω)) P

Exact module and namespace context

Lean proof · lawMapProdEqOfAEEq

The proof establishes equality of ordered pairs on a full-measure set, then reuses pushforward congruence. It does not posit independence of the coordinates.

theorem lawMapProdEqOfAEEq {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X X' : Ω → E} {Y Y' : Ω → F}
    (hX : X =ᵐ[P] X') (hY : Y =ᵐ[P] Y') :
    Measure.map (fun ω => (X ω, Y ω)) P =
      Measure.map (fun ω => (X' ω, Y' ω)) P := by
  exact Measure.map_congr <| by
    filter_upwards [hX, hY] with ω hx hy
    simp [hx, hy]

/-- First marginal of a paired pushforward law.

This is endpoint-law bookkeeping for common-space EM arguments: after a joint
endpoint law has been represented as a paired pushforward, projecting the first
coordinate recovers the first endpoint law.  Measurability is explicit; the
lemma does not construct any process, density, or conditional law.
-/

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.
As in map_congr, totalized map semantics apply without measurability. No conditional law or coupling construction is supplied.

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.