The composition-product of a measure and a kernel, in the reversed coordinate order

Mathlib's μ ⊗ₘ κ records the joint law of "draw q from μ, then p from κ q" as a measure on V × Ω, the base coordinate first. TauCeti.swapCompProd μ κ is that same joint law written on Ω × V, the kernel coordinate first, which is the order some product semigroups come in.

Everything Mathlib proves about ⊗ₘ transports across the swap, and this file records the transported statements that are awkward to reconstruct at each use: the mass of a measurable rectangle, the integral of a general function, the second marginal of a Markov composition, and — for a nonempty standard Borel kernel target — the converse, that every finite measure on Ω × V is such a composition over its second marginal.

Main declarations

• TauCeti.swapCompProd: the measure (μ ⊗ₘ κ).map Prod.swap on Ω × V, with TauCeti.swapCompProd_prod and TauCeti.lintegral_swapCompProd evaluating it.
• TauCeti.exists_eq_swapCompProd: every finite measure whose first coordinate is nonempty standard Borel is a TauCeti.swapCompProd over its second marginal, by disintegration.

noncomputable def TauCeti.swapCompProd {V : Type u_1} {Ω : Type u_2} [MeasurableSpace V] [MeasurableSpace Ω] (μ : MeasureTheory.Measure V) (κ : ProbabilityTheory.Kernel V Ω) : MeasureTheory.Measure (Ω × V)

The measure on Ω × V assembled from a measure μ on V and a kernel κ from V to Ω: draw the V coordinate from μ, then the Ω coordinate from κ, and swap the pair.

Equations

• TauCeti.swapCompProd μ κ = MeasureTheory.Measure.map Prod.swap (μ.compProd κ)

theorem TauCeti.swapCompProd_def {V : Type u_1} {Ω : Type u_2} [MeasurableSpace V] [MeasurableSpace Ω] (μ : MeasureTheory.Measure V) (κ : ProbabilityTheory.Kernel V Ω) : swapCompProd μ κ = MeasureTheory.Measure.map Prod.swap (μ.compProd κ)

The assembled measure is the swap-map of Mathlib's composition-product measure.

instance TauCeti.isFiniteMeasure_swapCompProd {V : Type u_1} {Ω : Type u_2} [MeasurableSpace V] [MeasurableSpace Ω] (μ : MeasureTheory.Measure V) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel V Ω) [ProbabilityTheory.IsFiniteKernel κ] : MeasureTheory.IsFiniteMeasure (swapCompProd μ κ)

theorem TauCeti.swapCompProd_prod {V : Type u_1} {Ω : Type u_2} [MeasurableSpace V] [MeasurableSpace Ω] (μ : MeasureTheory.Measure V) [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel V Ω) [ProbabilityTheory.IsSFiniteKernel κ] {A : Set Ω} (hA : MeasurableSet A) {B : Set V} (hB : MeasurableSet B) : (swapCompProd μ κ) (A ×ˢ B) = ∫⁻ (q : V) in B, (κ q) A ∂μ

The mass an assembled measure gives to a measurable rectangle: integrate the kernel mass of the first-coordinate side over the second-coordinate side.

theorem TauCeti.lintegral_swapCompProd {V : Type u_1} {Ω : Type u_2} [MeasurableSpace V] [MeasurableSpace Ω] (μ : MeasureTheory.Measure V) [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel V Ω) [ProbabilityTheory.IsSFiniteKernel κ] {f : Ω × V → ENNReal} (hf : Measurable f) : ∫⁻ (y : Ω × V), f y ∂swapCompProd μ κ = ∫⁻ (q : V), ∫⁻ (p : Ω), f (p, q) ∂κ q ∂μ

Integrating against an assembled measure means first integrating over the kernel fibre and then over the base measure.

@[simp]

theorem TauCeti.snd_swapCompProd {V : Type u_1} {Ω : Type u_2} [MeasurableSpace V] [MeasurableSpace Ω] (μ : MeasureTheory.Measure V) [MeasureTheory.SFinite μ] (κ : ProbabilityTheory.Kernel V Ω) [ProbabilityTheory.IsMarkovKernel κ] : (swapCompProd μ κ).snd = μ

The second marginal of an assembled measure is the measure it was assembled from.

theorem TauCeti.exists_eq_swapCompProd {V : Type u_1} {Ω : Type u_2} [MeasurableSpace V] [MeasurableSpace Ω] [StandardBorelSpace Ω] [Nonempty Ω] (μ : MeasureTheory.Measure (Ω × V)) [MeasureTheory.IsFiniteMeasure μ] : ∃ (κ : ProbabilityTheory.Kernel V Ω), ProbabilityTheory.IsMarkovKernel κ ∧ μ = swapCompProd μ.snd κ

Every finite measure on Ω × V is assembled from its second marginal and a Markov kernel. The kernel is the conditional distribution of the first coordinate given the second, which exists because Ω is a nonempty standard Borel space.