Sub-Probability Distributions

This file defines a type SPMF as a PMF extended with the option to fail. The probability of failure is the missing mass to make the PMF sum to 1.

def SPMF : Type u → Type u

A subprobability mass function is a function α → ℝ≥0∞ such that values have an infinite sum at most 1 represented by applying an OptionT transformer to the PMF monad. The new failure/none value holds the "missing" mass to reach the total sum of 1.

def SPMF.mk {α : Type u} (p : PMF (Option α)) : SPMF α

View a distribution on Option α as a subdistribution on α, where none is corresponds to the missing mass.

def SPMF.toPMF {α : Type u} (p : SPMF α) : PMF (Option α)

View a subdistribution on α as a distribution on Option α.

@[simp]

theorem SPMF.run_eq_toPMF {α : Type u} (p : SPMF α) : OptionT.run p = p.toPMF

@[simp]

theorem SPMF.toPMF_mk {α : Type u} (p : PMF (Option α)) : (SPMF.mk p).toPMF = p

@[simp]

theorem SPMF.mk_toPMF {α : Type u} (p : SPMF α) : SPMF.mk p.toPMF = p

noncomputable instance SPMF.instAlternativeMonad : AlternativeMonad SPMF

Expose the induced monad instance on SPMF.

instance SPMF.instLawfulAlternative : LawfulAlternative SPMF

instance SPMF.instLawfulMonad : LawfulMonad SPMF

noncomputable instance SPMF.instMonadLiftPMF : MonadLift PMF SPMF

Expose the lifting operations from PMF to SPMF given by OptionT.lift

instance SPMF.instLawfulMonadLiftPMF : LawfulMonadLift PMF SPMF

instance SPMF.instFunLikeENNReal {α : Type u} : FunLike (SPMF α) α ENNReal

Apply an SPMF α to an element of α.

theorem SPMF.apply_eq_toPMF_some {α : Type u} (p : SPMF α) (x : α) : p x = p.toPMF (some x)

theorem SPMF.liftM_eq_map {α : Type u} (p : PMF α) : liftM p = SPMF.mk (PMF.map some p)

@[simp]

theorem SPMF.lift_pure {α : Type u} (x : α) : liftM (PMF.pure x) = pure x

@[simp]

theorem SPMF.toPMF_liftM {α : Type u} (p : PMF α) : (liftM p).toPMF = do let a ← p pure (some a)

@[simp]

theorem SPMF.liftM_apply {α : Type u} (p : PMF α) (x : α) : (liftM p) x = p x

@[simp]

theorem SPMF.toPMF_pure {α : Type u} (x : α) : (pure x).toPMF = PMF.pure (some x)

theorem SPMF.failure_eq_mk {α : Type u} : failure = SPMF.mk (PMF.pure none)

@[simp]

theorem SPMF.toPMF_failure {α : Type u} : failure.toPMF = PMF.pure none

@[simp]

theorem SPMF.failure_apply {α : Type u} (x : α) : failure x = 0

noncomputable instance SPMF.instZero {α : Type u} : Zero (SPMF α)

theorem SPMF.zero_def {α : Type u} : 0 = failure

@[simp]

theorem SPMF.toPMF_zero {α : Type u} : SPMF.toPMF 0 = PMF.pure none

@[simp]

theorem SPMF.toPMF_bind {α β : Type u} (p : SPMF α) (q : α → SPMF β) : (p >>= q).toPMF = Option.elimM p.toPMF (PMF.pure none) fun (x : α) => (q x).toPMF

@[simp]

theorem SPMF.toPMF_map {α β : Type u} (p : SPMF α) (f : α → β) : (f <$> p).toPMF = Option.map f <$> p.toPMF

@[simp]

theorem SPMF.zero_apply {α : Type u} (x : α) : 0 x = 0

@[simp]

theorem SPMF.tsum_toPMF_some_add_toPMF_none {α : Type u} (p : SPMF α) : ∑' (x : α), p.toPMF (some x) + p.toPMF none = 1

@[simp]

theorem SPMF.run_none_add_tsum_run_some {α : Type u} (p : SPMF α) : p.toPMF none + ∑' (x : α), p.toPMF (some x) = 1

theorem SPMF.tsum_run_some_eq_one_sub {α : Type u} (p : SPMF α) : ∑' (x : α), p.toPMF (some x) = 1 - p.toPMF none

@[simp]

theorem SPMF.apply_ne_top {α : Type u} (p : SPMF α) (x : α) : p x ≠ ⊤

@[simp]

theorem SPMF.tsum_run_some_ne_top {α : Type u} (p : SPMF α) : ∑' (x : α), p.toPMF (some x) ≠ ⊤

theorem SPMF.run_none_eq_one_sub {α : Type u} (p : SPMF α) : p.toPMF none = 1 - ∑' (x : α), p.toPMF (some x)

theorem SPMF.ext {α : Type u} {p q : SPMF α} (h : ∀ (x : α), p x = q x) : p = q

theorem SPMF.ext_iff {α : Type u} {p q : SPMF α} : p = q ↔ ∀ (x : α), p x = q x

theorem SPMF.eq_liftM_iff_forall {α : Type u} (p : SPMF α) (q : PMF α) : p = liftM q ↔ ∀ (x : α), p x = q x

@[simp]

theorem SPMF.pure_apply {α : Type u} [DecidableEq α] (x y : α) : (pure x) y = if y = x then 1 else 0

@[simp]

theorem SPMF.pure_apply_self {α : Type u} (x : α) : (pure x) x = 1

@[simp]

theorem SPMF.pure_apply_eq_zero_iff {α : Type u} (x y : α) : (pure x) y = 0 ↔ y ≠ x

@[simp]

theorem SPMF.bind_apply_eq_tsum {α β : Type u} (p : SPMF α) (q : α → SPMF β) (y : β) : (p >>= q) y = ∑' (x : α), p x * (q x) y

def SPMF.support {α : Type u_1} (p : SPMF α) : Set α

The set of outputs with non-zero probability mass.

theorem SPMF.support_def {α : Type u} (p : SPMF α) : p.support = Function.support ⇑p

theorem SPMF.support_eq_preimage_some {α : Type u} (p : SPMF α) : p.support = some ⁻¹' p.toPMF.support

@[simp]

theorem SPMF.mem_support_iff {α : Type u} (p : SPMF α) (x : α) : x ∈ p.support ↔ p x ≠ 0

@[simp]

theorem SPMF.support_liftM {α : Type u} (p : PMF α) : (liftM p).support = p.support

@[simp]

theorem SPMF.support_pure {α : Type u} (x : α) : (pure x).support = {x}

@[simp]

theorem SPMF.map_mk {α β : Type u} (p : PMF (Option α)) (f : α → β) : f <$> SPMF.mk p = SPMF.mk (Option.map f <$> p)

@[reducible]

noncomputable def PMF.toSPMF' : PMF →ᵐ SPMF

Convert a PMF to an SPMF in the canonical way. dtumad: this should probably be a bare function with a hom-class instance.