Probability Distributions on Potentially Failing Computations

This file lifts MonadLiftT _ SetM and MonadLiftT _ SPMF semantics through the OptionT monad transformer, providing support, finSupport, and evalDist-based probability lemmas for OptionT m α in terms of the underlying m (Option α).

@[implicit_reducible]

noncomputable instance OptionT.instMonadLiftTSetM {m : Type u → Type v} [Monad m] [MonadLiftT m SetM] : MonadLiftT (OptionT m) SetM

Standalone MonadLiftT (OptionT m) SetM instance under the weaker [MonadLiftT m SetM] assumption. Keeping this standalone means support on OptionT m works without requiring a full MonadLiftT m SPMF lift — only MonadLiftT m SetM is needed.

We declare a MonadLiftT (rather than MonadLift) so the instance has no semiOutParam arguments to synthesize — OptionT m's m cannot be recovered from the SetM codomain.

instance OptionT.instLawfulMonadLiftTSetM {m : Type u → Type v} [Monad m] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] : LawfulMonadLiftT (OptionT m) SetM

theorem OptionT.support_def {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] (mx : OptionT m α) : support mx = some ⁻¹' support mx.run

@[simp]

theorem OptionT.mem_support_iff {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] (mx : OptionT m α) (x : α) : x ∈ support mx ↔ some x ∈ support mx.run

@[simp]

theorem OptionT.support_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] (mx : m α) : support (liftM mx) = support mx

@[simp]

theorem OptionT.support_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] (mx : m α) : support (OptionT.lift mx) = support mx

theorem OptionT.mem_support_bind_mk {m : Type u → Type v} [Monad m] {α β : Type u} [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] (sample : m α) (body : α → m (Option β)) {x : β} (hx : x ∈ support (OptionT.mk (sample >>= body))) : ∃ a ∈ support sample, x ∈ support (OptionT.mk (body a))

Peel the leading sample off the support of an OptionT.mk'd bind: any element of the support of OptionT.mk (sample >>= body) factors through a sample a in the support of sample, with the element in the support of OptionT.mk (body a).

@[implicit_reducible]

noncomputable instance OptionT.instHasEvalFinset (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] [HasEvalFinset m] : HasEvalFinset (OptionT m)

Lift a HasEvalFinset instance to OptionT. by just taking preimage under some.

theorem OptionT.finSupport_def {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [HasEvalFinset m] [DecidableEq α] (mx : OptionT m α) : finSupport mx = (finSupport mx.run).preimage some ⋯

@[simp]

theorem OptionT.mem_finSupport_iff {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [HasEvalFinset m] [DecidableEq α] (mx : OptionT m α) (x : α) : x ∈ finSupport mx ↔ some x ∈ finSupport mx.run

@[simp]

theorem OptionT.finSupport_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [HasEvalFinset m] [LawfulMonadLiftT m SetM] [LawfulMonad m] [DecidableEq α] (mx : m α) : finSupport (liftM mx) = finSupport mx

@[simp]

theorem OptionT.finSupport_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SetM] [HasEvalFinset m] [LawfulMonadLiftT m SetM] [LawfulMonad m] [DecidableEq α] (mx : m α) : finSupport (OptionT.lift mx) = finSupport mx

@[implicit_reducible]

noncomputable instance OptionT.instMonadLiftTSPMF (m : Type u → Type v) [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] : MonadLiftT (OptionT m) SPMF

Lift a MonadLiftT m SPMF instance to MonadLiftT (OptionT m) SPMF. Failure in OptionT contributes to the failure mass of the resulting SPMF.

instance OptionT.instLawfulMonadLiftTSPMF (m : Type u → Type v) [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] : LawfulMonadLiftT (OptionT m) SPMF

instance OptionT.instLawfulFailure (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] : HasEvalSet.LawfulFailure (OptionT m)

instance OptionT.instEvalDistCompatible (m : Type u → Type v) [Monad m] [MonadLiftT m SetM] [LawfulMonadLiftT m SetM] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [EvalDistCompatible m] : EvalDistCompatible (OptionT m)

The SetM-lift of OptionT m (preimage of support mx.run under some) agrees with the SPMF-lift (the OptionT.mapM' bind into SPMF) on outputs, given EvalDistCompatible m.

theorem OptionT.evalDist_eq {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : OptionT m α) : 𝒟[mx] = (fun {α : Type u} (x : OptionT m α) => (OptionT.mapM' (MonadHom.ofLift m SPMF)).toFun α x) mx

theorem OptionT.probOutput_eq {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : OptionT m α) (x : α) : Pr[= x | mx] = Pr[= some x | mx.run]

theorem OptionT.probEvent_eq {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : OptionT m α) (p : α → Prop) [DecidablePred p] : probEvent mx p + Pr[= none | mx.run] = probEvent mx.run fun (x : Option α) => Option.all (fun (b : α) => decide (p b)) x = true

theorem OptionT.probFailure_eq {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : OptionT m α) : Pr[⊥ | mx] = Pr[⊥ | mx.run] + Pr[= none | mx.run]

@[simp]

theorem OptionT.probOutput_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) (x : α) : Pr[= x | liftM mx] = Pr[= x | mx]

@[simp]

theorem OptionT.probOutput_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) (x : α) : Pr[= x | OptionT.lift mx] = Pr[= x | mx]

@[simp]

theorem OptionT.probEvent_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) (p : α → Prop) : probEvent (liftM mx) p = probEvent mx p

@[simp]

theorem OptionT.probEvent_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) (p : α → Prop) : probEvent (OptionT.lift mx) p = probEvent mx p

@[simp]

theorem OptionT.probFailure_liftM {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) : Pr[⊥ | liftM mx] = Pr[⊥ | mx]

@[simp]

theorem OptionT.probFailure_lift {m : Type u → Type v} [Monad m] {α : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : m α) : Pr[⊥ | OptionT.lift mx] = Pr[⊥ | mx]

theorem OptionT.probEvent_eq_of_run_map_eq {m : Type u → Type v} [Monad m] {α β : Type u} [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] [LawfulMonad m] (mx : OptionT m α) (my : OptionT m β) (f : β → α) (P : α → Prop) (h : mx.run = Option.map f <$> my.run) : probEvent mx P = probEvent my (P ∘ f)

Bridge lemma: when two OptionT computations have underlying runs related by an Option.map of a function f, their probabilities for the events P and P ∘ f agree.