Samplinglib mathematical lesson

Extract the second marginal of a joint image law

AutoSamplingTheory.lawMapProdSnd · theorem · Teaching coverage

Read this first

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

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.

Download module (.lean)

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

Proof roadmap

1Compose 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.
2Evaluate the composite
The selected projection or swap of a pair gives precisely the displayed target map, pointwise on Ω.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · lawMapProdSnd

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

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

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