Conditional branches under measure semantics

A proposition-valued observation selects between two computations. The resulting measure is the sum of the branch measures weighted by the selector's successful outcome masses. Discarded source values need no measurable space, and failure is kept separate from either branch.

@[simp]

theorem prEvent_false {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) : 𝒟[do let _ ← mx pure False] {True} = 0

An impossible final observation has zero mass, including after a failed computation.

theorem evalDist_bind_prop {m : Type → Type v} [Monad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {β : Type} [MeasurableSpace β] (selector : m Prop) (yes no : m β) : 𝒟[do let p ← selector if p then yes else no] = 𝒟[selector] {True} • 𝒟[yes] + 𝒟[selector] {False} • 𝒟[no]

Binding a propositional selector gives the two branch measures with their actual masses.

theorem prEvent_not_eq_apply_false {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) : 𝒟[do let x ← mx pure ¬p x] {True} = 𝒟[p <$> mx] {False}

An observation's negation is the false mass of the same propositional selector.

theorem prEvent_add_prEvent_not {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} + 𝒟[do let x ← mx pure ¬p x] {True} = 𝒟[p <$> mx] Set.univ

An event and its negation partition the selector's successful mass, including lossy draws.

theorem evalDist_bind_ite {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} [MeasurableSpace β] (mx : m α) (p : α → Prop) [DecidablePred p] (yes no : m β) : 𝒟[do let x ← mx if p x then yes else no] = 𝒟[do let x ← mx pure (p x)] {True} • 𝒟[yes] + 𝒟[do let x ← mx pure ¬p x] {True} • 𝒟[no]

A conditional continuation is a mixture weighted by the observed predicate, without a measurable space on discarded source values.

theorem measurable_evalDist_bind_ite {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {ρ : Type u_1} {α β : Type} [MeasurableSpace ρ] [MeasurableSpace β] (mx : ρ → m α) (p : ρ → α → Prop) [(r : ρ) → DecidablePred (p r)] (yes no : ρ → m β) (hobs : Measurable fun (r : ρ) => 𝒟[p r <$> mx r]) (hyes : Measurable fun (r : ρ) => 𝒟[yes r]) (hno : Measurable fun (r : ρ) => 𝒟[no r]) : Measurable fun (r : ρ) => 𝒟[do let x ← mx r if p r x then yes r else no r]

Measurable selector measures and branch measures give a measurable conditional family. The family can be bundled by evalDistKernel; discarded source values need no measurable space.

theorem evalDist.isProbabilityMeasure_bind_ite {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} [MeasurableSpace β] (mx : m α) (p : α → Prop) [DecidablePred p] [MeasureTheory.IsProbabilityMeasure 𝒟[p <$> mx]] (yes no : m β) [MeasureTheory.IsProbabilityMeasure 𝒟[yes]] [MeasureTheory.IsProbabilityMeasure 𝒟[no]] : MeasureTheory.IsProbabilityMeasure 𝒟[do let x ← mx if p x then yes else no]

Lossless branches selected by a lossless observation give a lossless computation. The selected output space may be continuous, and the discarded source needs no measurable space.

theorem prEvent_bind_ite {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β : Type} (mx : m α) (p : α → Prop) [DecidablePred p] (yes no : m β) (q : β → Prop) : 𝒟[do let y ← do let x ← mx if p x then yes else no pure (q y)] {True} = 𝒟[do let x ← mx pure (p x)] {True} * 𝒟[do let y ← yes pure (q y)] {True} + 𝒟[do let x ← mx pure ¬p x] {True} * 𝒟[do let y ← no pure (q y)] {True}

The event probability of a conditional continuation is the weighted sum of its two branch event probabilities. Each weight retains successful mass.

theorem prEvent_bind_eq_mul_of_ite {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α β γ : Type} (mx : m α) (f : α → m β) (p : α → Prop) [DecidablePred p] (q : β → Prop) (my : m γ) (r : γ → Prop) (h : ∀ (x : α), 𝒟[do let y ← f x pure (q y)] {True} = if p x then 𝒟[do let z ← my pure (r z)] {True} else 0) : 𝒟[do let y ← mx >>= f pure (q y)] {True} = 𝒟[do let x ← mx pure (p x)] {True} * 𝒟[do let z ← my pure (r z)] {True}

A continuation event that is constant on an observed condition and zero otherwise factors through that condition's probability. The reference event may have a different output type.