Probability Distributions on Option return types

File for lemmas about evalDist on involving Option.

@[simp]

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

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

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

theorem probEvent_isSome_eq_one_sub_probOutput_none {m : Type u → Type v} [Monad m] [HasEvalSPMF m] {α : Type u} (mx : m (Option α)) [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} [Monad m] [HasEvalSPMF m] {α : Type u} (mx : m (Option α)) [Fintype α] : ∑ x : α, Pr[= some x | mx] ≤ 1

@[simp]

theorem probOutput_some_map_option_map {m : Type u → Type v} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m (Option α)) {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} [Monad m] [LawfulMonad m] [HasEvalSPMF m] {α β : Type u} (mx : m (Option α)) (f : α → β) : Pr[= none | Option.map f <$> mx] = Pr[= none | mx]