ASTIS mathematical exposition

Extract the second marginal of a joint image law

AutoSamplingTheory.lawMapProdSnd · theorem · Teaching coverage

Statement

Let Ω,E,F be measurable spaces and P any measure on Ω. For measurable X:Ω→E and Y:Ω→F, pushing the joint law (X,Y)#P through its second projection gives Y#P.

\[\operatorname{snd}_\#((X,Y)_\#P)=Y_\#P.\]

All objects and hypotheses

Ω,E,F are arbitrary measurable spaces and P is any measure on Ω.
X:Ω→E and Y:Ω→F are both measurable, not merely assumed equal in law.

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

Mathematical proof

1. Compose the measurable maps

The pair map is measurable because both coordinates are. The projection or swap is measurable for product sigma-algebras, so consecutive pushforwards compose.

\[T_\#((X,Y)_\#P)=(T\circ(X,Y))_\#P.\]

Corresponding Lean step

Measure.map_map measurable_snd (hX.prod hY)

2. Evaluate the composite

The selected projection or swap of a pair gives precisely the displayed target map, pointwise on Ω.

\[\operatorname{snd}(X\omega,Y\omega)=Y\omega.\]

Corresponding Lean step

rfl

Lean statement · lawMapProdSnd

The two ordinary measurability hypotheses ensure this is genuine pushforward composition. The result identifies a measure, not a density.

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

Exact module and namespace context

Lean proof · lawMapProdSnd

One rewrite composes the maps; the remaining equality follows directly from how a pair's projection or swap is defined.

theorem lawMapProdSnd {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (hX : Measurable X) (hY : Measurable Y) :
    Measure.map Prod.snd (Measure.map (fun ω => (X ω, Y ω)) P) =
      Measure.map Y P := by
  rw [Measure.map_map measurable_snd (hX.prod hY)]
  rfl

/-- Swap the coordinate order of a paired pushforward law.

Mathlib conditional-distribution APIs usually represent the joint law for
`Y | X` in the order `(X,Y)`.  Some paper proofs first name the joint law in the
opposite order.  This helper records only the `Measure.map` orientation
bookkeeping; it does not construct a 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.
Only orientation/marginal bookkeeping; no independence, conditional kernel, process or density construction.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Measure.map_map
measurable_snd
Measurable.prod

Mathematical sources

Exact existing ASTIS declaration and body — Directly read local source; not a new proof or source-fidelity verdict.

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