Losslessness of measure-valued computations #
Losslessness is Mathlib's IsProbabilityMeasure on the successful-output measure. Bind preserves
this property when its continuation is lossless almost everywhere. Structurally possible
zero-probability branches impose no additional obligation.
theorem
evalDist.isProbabilityMeasure_map
{m : Type u → Type v}
[Monad m]
[EvalDistSemantics m]
[LawfulEvalDistSemantics m]
{α β : Type u}
[MeasurableSpace α]
[MeasurableSpace β]
[LawfulMonad m]
(mx : m α)
[MeasureTheory.IsProbabilityMeasure 𝒟[mx]]
{f : α → β}
(hf : Measurable f)
:
A measurable output map preserves losslessness on the chosen output spaces.
theorem
evalDist.isProbabilityMeasure_bind_of_ae
{m : Type u → Type v}
[Monad m]
[EvalDistSemantics m]
[LawfulEvalDistSemantics m]
{α β : Type u}
[MeasurableSpace α]
[MeasurableSpace β]
(mx : m α)
(f : α → m β)
[MeasureTheory.IsProbabilityMeasure 𝒟[mx]]
(hf : Measurable fun (a : α) => 𝒟[f a])
(hprob : ∀ᵐ (a : α) ∂𝒟[mx], MeasureTheory.IsProbabilityMeasure 𝒟[f a])
:
A lossless computation followed by almost everywhere lossless continuations is lossless.
theorem
evalDist.isProbabilityMeasure_bind_iff
{m : Type u → Type v}
[Monad m]
[EvalDistSemantics m]
[LawfulEvalDistSemantics m]
{α β : Type u}
[MeasurableSpace α]
[MeasurableSpace β]
(mx : m α)
(f : α → m β)
[MeasureTheory.IsProbabilityMeasure 𝒟[mx]]
(hf : Measurable fun (a : α) => 𝒟[f a])
:
For a lossless input, losslessness after bind means almost everywhere lossless continuation.
theorem
evalDist.isProbabilityMeasure_bind
{m : Type u → Type v}
[Monad m]
[EvalDistSemantics m]
[LawfulEvalDistSemantics m]
{α β : Type u}
[MeasurableSpace α]
[MeasurableSpace β]
(mx : m α)
(f : α → m β)
[DiscreteMeasurableSpace α]
[MeasureTheory.IsProbabilityMeasure 𝒟[mx]]
(hprob : ∀ (a : α), MeasureTheory.IsProbabilityMeasure 𝒟[f a])
:
Pointwise losslessness is a sufficient discrete bind rule with no source-space argument.