Monotonicity and ω-continuity of the Giry monad #
Measure.bind is monotone in both arguments and commutes with suprema of monotone sequences in
both arguments. Together with the complete lattice structure on Measure α, this makes an
operator built from bind ω-Scott-continuous, so its least fixed point is the supremum of its
Kleene iterates (fixedPoints.lfp_eq_sSup_iterate). This is the least-fixed-point semantics of
recursive probabilistic programs of [Koz81], stated on the monad of [Gir82].
[UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/GiryMonad.lean.
Main results #
MeasureTheory.Measure.bind_mono:bindis monotone in the measure and in the kernel.MeasureTheory.Measure.iSup_apply_of_monotone: the supremum of a monotone sequence of measures is computed pointwise on measurable sets.MeasureTheory.lintegral_iSup_measure_of_monotone: Lebesgue integrals commute with monotone suprema of measures.MeasureTheory.Measure.iSup_bind_of_monotone,MeasureTheory.Measure.bind_iSup_of_monotone:bindcommutes with monotone suprema in each argument.MeasureTheory.Measure.ωScottContinuous_bind,MeasureTheory.Measure.ωScottContinuous_map,MeasureTheory.Measure.ωScottContinuous_prod:bindis ω-Scott-continuous jointly in the measure and the kernel,mapin the measure andprodin both factors, so operators built from them have Kleene least fixed points.
Implementation notes #
Measure α is an ω-complete partial order through its complete lattice, while a Pi type of
measures also carries the product ω-CPO instance; the two agree but not reducibly, so continuity
proofs are pinned to explicit suprema through CompleteLattice.ωSup_eq_iSup and
Pi.ωSup_eq_iSup rather than to ωSup.
References #
theorem
ENNReal.iSup_tsum_of_monotone
{ι : Type u_1}
{g : ℕ → ι → ENNReal}
(hg : Monotone g)
:
⨆ (n : ℕ), ∑' (i : ι), g n i = ∑' (i : ι), ⨆ (n : ℕ), g n i
A supremum over a monotone sequence commutes with a countable sum.
theorem
MeasureTheory.Measure.bind_mono_left
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ ν : Measure α}
{f : α → Measure β}
(hμν : μ ≤ ν)
(hf : AEMeasurable f ν)
:
μ.bind f ≤ ν.bind f
theorem
MeasureTheory.Measure.bind_mono_right
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{f g : α → Measure β}
(hfg : ∀ (a : α), f a ≤ g a)
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
μ.bind f ≤ μ.bind g
theorem
MeasureTheory.Measure.bind_mono
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ ν : Measure α}
{f g : α → Measure β}
(hμν : μ ≤ ν)
(hfg : ∀ (a : α), f a ≤ g a)
(hf : AEMeasurable f μ)
(hg : AEMeasurable g ν)
:
μ.bind f ≤ ν.bind g
theorem
MeasureTheory.Measure.iSup_apply_of_monotone
{α : Type u_1}
[MeasurableSpace α]
{μ : ℕ → Measure α}
(hμ : Monotone μ)
{s : Set α}
(hs : MeasurableSet s)
:
(⨆ (n : ℕ), μ n) s = ⨆ (n : ℕ), (μ n) s
The supremum of a monotone sequence of measures is computed pointwise on measurable sets.
theorem
MeasureTheory.SimpleFunc.lintegral_iSup_measure_of_monotone
{α : Type u_1}
[MeasurableSpace α]
{μ : ℕ → Measure α}
(hμ : Monotone μ)
(g : SimpleFunc α ENNReal)
:
g.lintegral (⨆ (n : ℕ), μ n) = ⨆ (n : ℕ), g.lintegral (μ n)
Simple-function integrals commute with monotone suprema of measures.
theorem
MeasureTheory.lintegral_iSup_measure_of_monotone
{α : Type u_1}
[MeasurableSpace α]
{μ : ℕ → Measure α}
(hμ : Monotone μ)
(f : α → ENNReal)
:
∫⁻ (a : α), f a ∂⨆ (n : ℕ), μ n = ⨆ (n : ℕ), ∫⁻ (a : α), f a ∂μ n
Lebesgue integrals commute with monotone suprema of measures.
theorem
MeasureTheory.Measure.iSup_bind_of_monotone
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : ℕ → Measure α}
(hμ : Monotone μ)
{f : α → Measure β}
(hf : Measurable f)
:
(⨆ (n : ℕ), μ n).bind f = ⨆ (n : ℕ), (μ n).bind f
theorem
MeasureTheory.Measure.measurable_iSup_measure_of_monotone
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : ℕ → α → Measure β}
(hf : ∀ (n : ℕ), Measurable (f n))
(hmono : Monotone f)
:
Measurable fun (a : α) => ⨆ (n : ℕ), f n a
theorem
MeasureTheory.Measure.bind_iSup_of_monotone
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : Measure α}
{f : ℕ → α → Measure β}
(hf : ∀ (n : ℕ), Measurable (f n))
(hmono : Monotone f)
:
(μ.bind fun (a : α) => ⨆ (n : ℕ), f n a) = ⨆ (n : ℕ), μ.bind (f n)
ω-Scott continuity #
theorem
MeasureTheory.Measure.ωScottContinuous_bind
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{γ : Type u_3}
[OmegaCompletePartialOrder γ]
{M : γ → Measure α}
{F : γ → α → Measure β}
(hM : OmegaCompletePartialOrder.ωScottContinuous M)
(hF : ∀ (a : α), OmegaCompletePartialOrder.ωScottContinuous fun (x : γ) => F x a)
(hmeas : ∀ (x : γ), Measurable (F x))
:
OmegaCompletePartialOrder.ωScottContinuous fun (x : γ) => (M x).bind (F x)
bind is ω-Scott-continuous jointly in the measure and the kernel.
theorem
MeasureTheory.Measure.ωScottContinuous_map
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{γ : Type u_3}
[OmegaCompletePartialOrder γ]
{M : γ → Measure α}
(hM : OmegaCompletePartialOrder.ωScottContinuous M)
{g : α → β}
(hg : Measurable g)
:
OmegaCompletePartialOrder.ωScottContinuous fun (x : γ) => map g (M x)
theorem
MeasureTheory.Measure.ωScottContinuous_prod
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{γ : Type u_3}
[OmegaCompletePartialOrder γ]
{M : γ → Measure α}
{N : γ → Measure β}
(hM : OmegaCompletePartialOrder.ωScottContinuous M)
(hN : OmegaCompletePartialOrder.ωScottContinuous N)
[∀ (x : γ), SFinite (N x)]
:
OmegaCompletePartialOrder.ωScottContinuous fun (x : γ) => (M x).prod (N x)
theorem
MeasureTheory.Measure.ωScottContinuous_bind_left
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{f : α → Measure β}
(hf : Measurable f)
:
OmegaCompletePartialOrder.ωScottContinuous fun (μ : Measure α) => μ.bind f
theorem
MeasureTheory.Measure.ωScottContinuous_bind_right
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{γ : Type u_3}
[OmegaCompletePartialOrder γ]
{μ : Measure α}
{F : γ → α → Measure β}
(hF : ∀ (a : α), OmegaCompletePartialOrder.ωScottContinuous fun (x : γ) => F x a)
(hmeas : ∀ (x : γ), Measurable (F x))
:
OmegaCompletePartialOrder.ωScottContinuous fun (x : γ) => μ.bind (F x)