Probability Distributions on Option return types

Lemmas about evalSPMF and the associated probabilities for computations returning an Option.

@[simp]

theorem probOutput_some_map_some {m : Type u → Type v} {α : Type u} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : m α) (x : α) : Pr[= some x | some <$> mx] = Pr[= x | mx]

@[simp]

theorem probOutput_some_map_none {m : Type u → Type v} {α : Type u} [Monad m] [LawfulMonad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : m α) : Pr[= none | some <$> mx] = 0

theorem probOutput_none_add_tsum_some {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m (Option α)) : Pr[= none | mx] + ∑' (x : α), Pr[= some x | mx] = 1 - Pr[⊥ | mx]

theorem probEvent_isSome_eq_tsum_probOutput_some {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m (Option α)) : (probEvent mx fun (r : Option α) => r.isSome = true) = ∑' (x : α), Pr[= some x | mx]

The probability of returning some is the total mass of all some outputs, without requiring the computation to be failure-free.

theorem sum_probEvent_option_map_eq_some_le_isSome {m : Type u → Type v} {α γ : Type u} [MonadLiftT m SPMF] (mx : m (Option α)) [Fintype γ] (select : α → Option γ) : (∑ k : γ, probEvent mx fun (r : Option α) => Option.map select r = some (some k)) ≤ probEvent mx fun (r : Option α) => r.isSome = true

Selector fibers inside an optional output are disjoint, so their finite sum is bounded by the probability of returning any some value.

theorem probEvent_isSome_eq_one_sub_probOutput_none {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m (Option α)) [Monad m] [NeverFail mx] : (probEvent mx fun (r : Option α) => r.isSome = true) = 1 - Pr[= none | mx]

theorem sum_probOutput_some_le_one {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m (Option α)) [Fintype α] : ∑ x : α, Pr[= some x | mx] ≤ 1

@[simp]

theorem probOutput_some_map_option_map {m : Type u → Type v} {α β : Type u} [MonadLiftT m SPMF] (mx : m (Option α)) [Monad m] [LawfulMonad m] [LawfulMonadLiftT m SPMF] {f : α → β} (hf : Function.Injective f) (x : α) : Pr[= some (f x) | Option.map f <$> mx] = Pr[= some x | mx]

@[simp]

theorem probOutput_none_map_option_map {m : Type u → Type v} {α β : Type u} [MonadLiftT m SPMF] (mx : m (Option α)) [Monad m] [LawfulMonad m] [LawfulMonadLiftT m SPMF] (f : α → β) : Pr[= none | Option.map f <$> mx] = Pr[= none | mx]