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.

theorem PMF.eq_pure_of_forall_ne_eq_zero {γ : Type u_1} (p : PMF γ) (a : γ) (h : ∀ (x : γ), x ≠ a → p x = 0) : p = pure a

A PMF that is zero at all points except a equals PMF.pure a.

theorem PMF.bind_congr {γ : Type u_1} {δ : Type u_2} (p : PMF γ) (f g : γ → PMF δ) (h : ∀ (x : γ), p x ≠ 0 → f x = g x) : p.bind f = p.bind g

PMF.bind respects equality on the support.

theorem PMF.map_eq_pure_zero {γ : Type u_1} {δ : Type u_2} (f : γ → δ) (c : PMF γ) (b : δ) (h : map f c = pure b) (a : γ) (ha : f a ≠ b) : c a = 0

If PMF.map f c = PMF.pure b and f a ≠ b, then c a = 0.

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.

Equations

• SPMF = OptionT PMF

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.

Equations

• SPMF.mk p = OptionT.mk p

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

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

Equations

• p.toPMF = OptionT.run p

@[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.

Equations

• SPMF.instAlternativeMonad = OptionT.instAlternativeMonadOfMonad PMF

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

Equations

• SPMF.instMonadLiftPMF = { monadLift := fun {α : Type ?u.5} => OptionT.lift }

instance SPMF.instLawfulMonadLiftPMF : LawfulMonadLift PMF SPMF

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

Apply an SPMF α to an element of α.

Equations

• SPMF.instFunLikeENNReal = { coe := fun (p : SPMF α) (x : α) => (OptionT.run p) (some x), coe_injective' := ⋯ }

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 α)

Equations

• SPMF.instZero = { zero := failure }

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

@[simp]

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

@[simp]

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

@[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.mk_pure_some {α : Type u} (x : α) : SPMF.mk (PMF.pure (some x)) = pure x

@[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

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

@[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.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.

Equations

• p.support = Function.support ⇑p

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}

def SPMF.gap {α : Type u} (p : SPMF α) : ENNReal

Gap between the total mass of p : SPMF and 1, so ∑ x, p x + p.gap = 1. TODO: use this to simplify the API around failure and needing toPMF/run.

Equations

• p.gap = p.toPMF none

theorem SPMF.gap_eq_toPMF_none {α : Type u} (p : SPMF α) : p.gap = p.toPMF none

theorem SPMF.gap_eq_one_sub_tsum {α : Type u} (p : SPMF α) : p.gap = 1 - ∑' (x : α), p x

theorem SPMF.toReal_gap_eq_one_sub_sum_toReal {α : Type u} [Fintype α] (p : SPMF α) : p.gap.toReal = 1 - ∑ x : α, (p x).toReal

@[simp]

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

theorem SPMF.bind_eq_pmf_bind {α β : Type u} {p : SPMF α} {f : α → SPMF β} : p >>= f = PMF.bind p fun (a : Option α) => match a with | some a' => f a' | none => PMF.pure none

@[simp]

theorem SPMF.PMF.map_some_apply_some {α : Type u} (p : PMF α) (x : α) : (some <$> p) (some x) = p x

theorem SPMF.pure_eq_pure_some {α : Type u} (a : α) : pure a = SPMF.mk (PMF.pure (some a))

pure a in SPMF equals PMF.pure (some a) as a PMF on Option α.

@[simp]

theorem SPMF.toPMF_inj {α : Type u} (p q : SPMF α) : p.toPMF = q.toPMF ↔ p = q

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

The functor map for SPMF equals PMF.map (Option.map f).