Events of optional computations

Native successful-output semantics turns a sampled guard into a condition on the sampled value. The intermediate measurable space is internal to the observation law. Wrapped computations are observed through their present values, and sequencing a lossless prefix with continuations that succeed on its reachable outputs preserves probability-one events.

theorem OptionT.prEvent_eq_run {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : OptionT m α) (p : α → Prop) : 𝒟[do let x ← mx pure (p x)] {True} = 𝒟[do let value ← mx.run pure (value.elim False p)] {True}

Successful events are the events of present values in the underlying run.

@[simp]

theorem OptionT.prEvent_lift {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) : 𝒟[do let x ← OptionT.lift mx pure (p x)] {True} = 𝒟[do let x ← mx pure (p x)] {True}

Lifting into the optional monad preserves the probability of an observed event.

@[simp]

theorem OptionT.prEvent_bind_guard {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p q : α → Prop) [DecidablePred p] : 𝒟[do let x ← OptionT.lift mx guard (p x) pure (q x)] {True} = 𝒟[do let x ← mx pure (p x ∧ q x)] {True}

A guard contributes its condition to the observed event after a lifted draw.

@[simp]

theorem OptionT.prEvent_bind_map_guard {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p q : α → Prop) [DecidablePred p] : 𝒟[do let x ← OptionT.lift mx (fun (x_1 : Unit) => q x) <$> guard (p x)] {True} = 𝒟[do let x ← mx pure (p x ∧ q x)] {True}

A constant map after a sampled guard contributes its guard to the observed event.

@[simp]

theorem OptionT.evalDist_lift_bind_guard {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) [DecidablePred p] : 𝒟[do let x ← OptionT.lift mx guard (p x)] = 𝒟[do let x ← mx pure (p x)] {True} • MeasureTheory.Measure.dirac ()

A lifted draw followed by a guard puts its successful event mass at the unit output.

@[simp]

theorem OptionT.evalDist_liftM_bind_guard {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m α) (p : α → Prop) [DecidablePred p] : 𝒟[do let x ← liftM mx guard (p x)] = 𝒟[do let x ← mx pure (p x)] {True} • MeasureTheory.Measure.dirac ()

A monadic lift followed by a guard puts its successful event mass at the unit output.

theorem OptionT.prEvent_mk {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] {α : Type} (mx : m (Option α)) (p : α → Prop) : 𝒟[do let x ← OptionT.mk mx pure (p x)] {True} = 𝒟[do let o ← mx pure (o.elim False p)] {True}

A successful event of a wrapped computation is the event of present values that satisfy it in the underlying computation.

theorem OptionT.mem_support_of_mem_support_lift {m : Type → Type v} [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] {α : Type} {mx : m α} {a : α} (ha : a ∈ support (OptionT.lift mx)) : a ∈ support mx

Reachable outputs of a lifted computation are reachable in the computation.

theorem OptionT.mk_bind_eq_lift_bind {m : Type → Type v} [Monad m] [LawfulMonad m] {α β : Type} (mx : m α) (f : α → m (Option β)) : OptionT.mk (mx >>= f) = do let a ← OptionT.lift mx OptionT.mk (f a)

A wrapped bind is a lifted prefix followed by the wrapped continuations.

theorem OptionT.prEvent_mk_bind_eq_one_of_support {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] [MonadAttach m] [ExactMonadAttach m] {α β : Type} (mx : m α) (hmx : 𝒟[do let _ ← mx pure True] {True} = 1) (f : α → m (Option β)) (p : β → Prop) (h : ∀ a ∈ support mx, 𝒟[do let y ← OptionT.mk (f a) pure (p y)] {True} = 1) : 𝒟[do let y ← OptionT.mk (mx >>= f) pure (p y)] {True} = 1

A lossless prefix followed by continuations that each satisfy an event with probability one on the prefix's reachable outputs satisfies the event with probability one.

theorem OptionT.prEvent_mk_bind_le_of_forall_le {m : Type → Type v} [Monad m] [LawfulMonad m] [EvalDistSemantics m] [LawfulEvalDistSemantics m] [MonadAttach m] [ExactMonadAttach m] {α β : Type} (mx : m α) (f : α → m (Option β)) (q : β → Prop) {ε : ENNReal} (h : ∀ a ∈ support mx, 𝒟[do let y ← OptionT.mk (f a) pure (q y)] {True} ≤ ε) : 𝒟[do let y ← OptionT.mk (mx >>= f) pure (q y)] {True} ≤ ε

An upper bound on the wrapped continuation event over reachable prefixes.