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] : Pr[fun (r : Option α) => r.isSome = true | mx] = 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 α)) [DecidableEq β] (f : α → β) : Pr[=none | Option.map f <$> mx] = Pr[=none | mx]