The Giry monad's map/bind interchange laws

Two ways Measure.map and Measure.bind commute:

• map_bind — pushing a mixture forward is the mixture of the pushforwards, map F ∘ bind g = bind (map F ∘ g);
• bind_map — binding after a pushforward reindexes the mixing measure, bind g ∘ map f = bind (g ∘ f).

Mathlib carries both for PMF (PMF.map_bind, PMF.bind_map) but neither for Measure, although all of their ingredients — Measure.bind_bind, Measure.bind_dirac_eq_map, Measure.dirac_bind — are there. This file supplies the missing Measure forms.

They are the shape mixture arguments want: bind is how a random measure is integrated against its mixing law, so pushing a mixture forward along a coordinate map (a marginal), or rewriting a mixture over a pushforward mixing law, are both routine steps.

theorem TauCeti.MeasureTheory.map_bind {S : Type u_1} {γ : Type u_2} {δ : Type u_3} [MeasurableSpace S] [MeasurableSpace γ] [MeasurableSpace δ] {μ : MeasureTheory.Measure S} {g : S → MeasureTheory.Measure γ} (hg : AEMeasurable g μ) {F : γ → δ} (hF : Measurable F) : MeasureTheory.Measure.map F (μ.bind g) = μ.bind fun (ω : S) => MeasureTheory.Measure.map F (g ω)

Naturality of bind. Pushing a Measure.bind mixture forward by a measurable map commutes with the bind: the pushforward of the mixture is the mixture of the pushforwards, i.e. the Giry-monad identity map F ∘ bind g = bind (map F ∘ g).

Obtained from associativity of bind together with bind_dirac_eq_map.

@[simp]

theorem TauCeti.MeasureTheory.bind_map {S : Type u_1} {γ : Type u_2} {δ : Type u_3} [MeasurableSpace S] [MeasurableSpace γ] [MeasurableSpace δ] {μ : MeasureTheory.Measure S} {f : S → γ} (hf : AEMeasurable f μ) {g : γ → MeasureTheory.Measure δ} (hg : AEMeasurable g (MeasureTheory.Measure.map f μ)) : (MeasureTheory.Measure.map f μ).bind g = μ.bind (g ∘ f)

Binding after a pushforward. Binding g against a pushforward measure reindexes the mixing measure: bind g ∘ map f = bind (g ∘ f).

This is the Measure form of PMF.bind_map, and like it is a simp lemma: it rewrites a bind of a mapped measure into the canonical single-bind form.