Measure-valued computation laws

The Giry composition laws transport measure-level independence to computation syntax. The general interchange theorem requires joint measurability; the three-draw law specializes to discrete intermediate results and leaves the final result space arbitrary. Uniform finite draws can be reindexed by a bijection before an arbitrary continuation.

theorem evalDist_bind_bijective_of_uniform {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] [LawfulMonad m] [DiscreteMeasurableSpace α] [MeasurableSingletonClass α] [Finite α] [Nonempty α] (mx : m α) (huniform : 𝒟[mx] = ProbabilityTheory.uniformOn Set.univ) (e : α → α) (he : Function.Bijective e) (f : α → m β) : 𝒟[do let x ← mx f (e x)] = 𝒟[mx >>= f]

Reindexing a uniform draw by a bijection does not change the measure of any subsequent computation. The uniformity hypothesis can come from either native sampling or a compatibility certificate.

theorem evalDist_bind_bijective_uniform_cross {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [LawfulMonad m] [DiscreteMeasurableSpace α] [DiscreteMeasurableSpace β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] [Finite α] [Finite β] [Nonempty α] [Nonempty β] (mx : m α) (my : m β) (hα : 𝒟[mx] = ProbabilityTheory.uniformOn Set.univ) (hβ : 𝒟[my] = ProbabilityTheory.uniformOn Set.univ) (e : α → β) (he : Function.Bijective e) (f : β → m γ) : 𝒟[do let x ← mx f (e x)] = 𝒟[my >>= f]

A bijection transports a uniform draw to a possibly different uniformly sampled type before an arbitrary continuation.

theorem evalDist_bind_bind_swap {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] (mx : m α) (my : m β) (f : α → β → m γ) (hf : Measurable fun (p : α × β) => 𝒟[f p.1 p.2]) : 𝒟[do let a ← mx let b ← my f a b] = 𝒟[do let b ← my let a ← mx f a b]

Independent computations commute under a jointly measurable denoted continuation.

theorem evalDist_bind_bind_swap_of_countable {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [Countable α] [Countable β] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (mx : m α) (my : m β) (f : α → β → m γ) : 𝒟[do let a ← mx let b ← my f a b] = 𝒟[do let b ← my let a ← mx f a b]

Independent countable draws with measurable singletons commute before any continuation. The selected source spaces make joint measurability automatic.

theorem evalDist_bind_bind_bind_rotate {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ δ : Type u} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] [DiscreteMeasurableSpace α] [DiscreteMeasurableSpace β] [DiscreteMeasurableSpace γ] (mx : m α) (my : m β) (mz : m γ) (f : α → β → γ → m δ) (hf : Measurable fun (p : α × β × γ) => 𝒟[f p.1 p.2.1 p.2.2]) : 𝒟[do let a ← mx let b ← my let c ← mz f a b c] = 𝒟[do let c ← mz let a ← mx let b ← my f a b c]

Move the third independent discrete draw to the front of a computation.

theorem evalDist_bind_apply_mono {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f g : α → m β) (hf : Measurable fun (a : α) => 𝒟[f a]) (hg : Measurable fun (a : α) => 𝒟[g a]) {event : Set β} (hevent : MeasurableSet event) (hfg : ∀ᵐ (a : α) ∂𝒟[mx], 𝒟[f a] event ≤ 𝒟[g a] event) : 𝒟[mx >>= f] event ≤ 𝒟[mx >>= g] event

Compare event masses after a common draw using an almost-everywhere continuation bound.

theorem le_evalDist_bind_apply {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) [MeasureTheory.IsProbabilityMeasure 𝒟[mx]] (f : α → m β) (hf : Measurable fun (a : α) => 𝒟[f a]) {event : Set β} (hevent : MeasurableSet event) {bound : ENNReal} (hbound : ∀ᵐ (a : α) ∂𝒟[mx], bound ≤ 𝒟[f a] event) : bound ≤ 𝒟[mx >>= f] event

A lower bound on continuation event masses holds after a lossless common draw.

theorem evalDist_bind_apply_mono_of_discrete {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace α] (mx : m α) (f g : α → m β) {event : Set β} (hevent : MeasurableSet event) (hfg : ∀ (a : α), 𝒟[f a] event ≤ 𝒟[g a] event) : 𝒟[mx >>= f] event ≤ 𝒟[mx >>= g] event

For a discrete common draw, a pointwise continuation bound suffices.

theorem evalDist_bind_apply_le_add_of_bad {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) (hf : Measurable fun (a : α) => 𝒟[f a]) {bad : Set α} (hbad : MeasurableSet bad) {event : Set β} (hevent : MeasurableSet event) {ε₁ ε₂ : ENNReal} (hbadBound : 𝒟[mx] bad ≤ ε₁) (hgood : ∀ a ∉ bad, 𝒟[f a] event ≤ ε₂) : 𝒟[mx >>= f] event ≤ ε₁ + ε₂

Charge a bad intermediate event separately from uniformly bounded good continuations.

theorem evalDist_bind_apply_le_add_lintegral_of_bad {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f : α → m β) (hf : Measurable fun (a : α) => 𝒟[f a]) {bad : Set α} (hbad : MeasurableSet bad) {event : Set β} (hevent : MeasurableSet event) (bound : α → ENNReal) {ε : ENNReal} (hgood : ∀ᵐ (a : α) ∂𝒟[mx], a ∉ bad → 𝒟[f a] event ≤ bound a + ε) : 𝒟[mx >>= f] event ≤ 𝒟[mx] bad + ε + ∫⁻ (a : α), bound a ∂𝒟[mx]

Charge a bad intermediate event and integrate an almost-everywhere continuation bound.

theorem evalDist_bind_apply_le_add_of_disagree {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type u} [MeasurableSpace α] [MeasurableSpace β] (mx : m α) (f g : α → m β) (hf : Measurable fun (a : α) => 𝒟[f a]) (hg : Measurable fun (a : α) => 𝒟[g a]) {bad : Set α} (hbad : MeasurableSet bad) {event : Set β} (hevent : MeasurableSet event) {ε : ENNReal} (hgood : ∀ᵐ (a : α) ∂𝒟[mx], a ∉ bad → 𝒟[f a] event ≤ 𝒟[g a] event + ε) : 𝒟[mx >>= f] event ≤ 𝒟[mx >>= g] event + 𝒟[mx] bad + ε

Compare two denoted continuations outside a measurable disagreement set.

Reachability and measurable observations

theorem evalDist.ae_of_forall_mem_support {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type u} [MeasurableSpace α] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] (mx : m α) (p : α → Prop) (hp : MeasurableSet {x : α | p x}) (h : ∀ x ∈ support mx, p x) : ∀ᵐ (x : α) ∂𝒟[mx], p x

A measurable predicate holding on every possible output holds almost everywhere under the successful-output measure. Core attachment supplies a subtype of possible outputs, and its measurable projection recovers the original computation.

theorem evalDist.apply_eq_zero_of_disjoint_support {m : Type u → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type u} [MeasurableSpace α] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] (mx : m α) {event : Set α} (hevent : MeasurableSet event) (h : ∀ x ∈ support mx, x ∉ event) : 𝒟[mx] event = 0

A measurable event containing no possible output has zero successful mass.