Swap the coordinate order of a joint image law

AutoSamplingTheory.lawMapProdSwap · 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 coordinate swap gives the joint law (Y,X)#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

theorem lawMapProdSwap {Ω E F : Type*} [MeasurableSpace Ω]
    [MeasurableSpace E] [MeasurableSpace F]
    {P : Measure Ω} {X : Ω → E} {Y : Ω → F}
    (hX : Measurable X) (hY : Measurable Y) :
    Measure.map Prod.swap (Measure.map (fun ω => (X ω, Y ω)) P) =
      Measure.map (fun ω => (Y ω, X ω)) P

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

/-- Mathlib orientation bridge between `condDistrib` and `condExpKernel`.

For the SALD conditional drift, instantiate `Y` with `X_k^eta` and `X` with
`hat X_s`: the conditional distribution of `X_k^eta` given `hat X_s` agrees
almost everywhere with the conditional-expectation kernel mapped by `X_k^eta`.
This is a local theorem from Mathlib's conditional-kernel backend, not a weak
Fokker--Planck or KL differentiability result.
-/

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.