Typeclasses for Denotational Monad Semantics

This file builds atop MonadLiftT m SPMF / MonadLiftT m PMF for assigning denotational probability semantics to monadic computations. We also introduce functions probOutput, probEvent, and probFailure with associated notation.

-- dtumad: document various probability notation definitions here

MonadLiftT m SetM and MonadLiftT m SPMF

The SetM / SPMF lifts exposed by this layer are declared as MonadLiftT, not MonadLift. Total semantic sources may still expose a plain MonadLift into PMF; the important point here is that support is never obtained by a transitive m → SPMF → SetM path, and parameterized/typeclass-gated probability lifts avoid MonadLift instance search. There are two independent reasons.

No transitive SPMF → SetM lift. The MonadLiftT SPMF SetM instance below exists so support and friends work on raw SPMF α. Crucially it is declared as MonadLiftT rather than MonadLift, which means Lean's monadLiftTrans (which requires MonadLift n o for the outer hop) cannot chain it: a monad m with MonadLiftT m SPMF does not automatically gain MonadLiftT m SetM via transitivity. Each monad declares its MonadLiftT m SetM directly — e.g. OracleComp uses the syntactic simulateQ into SetM (which doesn't require [spec.Fintype]), and EvalDistCompatible records the propositional coherence between that syntactic support and SPMF.support ∘ evalDist.

Resolution fragility for parameterized + typeclass-gated lifts. Lifts whose source is parameterized (OracleComp spec, OptionT m, StateT σ m, …) and which are gated by a typeclass on the parameter ([IsProbabilitySpec spec], [MonadLiftT m SPMF], …) must also be MonadLiftT, not MonadLift. Demoting to MonadLift forces Lean to find the instance through its transitive instance, whose outer hop is MonadLift n o with n a semiOutParam. When the recursion lands on a parameterized head like MonadLift (OracleComp ?spec) PMF, Lean has to simultaneously unify ?spec through the semiOutParam, discharge the typeclass premise on ?spec, and pin down ?spec from the inner reflexive premise — a combination Lean's instance search refuses to chase. The direct MonadLiftT declaration sidesteps this with a single-step head match.

@[implicit_reducible]

instance instMonadLiftTSPMFSetM : MonadLiftT SPMF SetM

Direct MonadLiftT SPMF SetM (only on SPMF itself — not the transitive MonadLift that would create a diamond).

instance instLawfulMonadLiftTSPMFSetM : LawfulMonadLiftT SPMF SetM

class EvalDistCompatible (m : Type u → Type v) [MonadLiftT m SetM] [MonadLiftT m SPMF] : Prop

Coherence between support (via MonadLiftT m SetM) and evalDist (via MonadLiftT m SPMF): x ∈ support mx iff Pr[= x | mx] ≠ 0.

This typeclass is exported by every monad that admits both lifts and they agree on outputs — i.e. support mx = SPMF.support (evalDist mx).

• support_eq_SPMF_support {α : Type u} (mx : m α) : (liftM mx).run = (liftM mx).support

  The reachable outputs of mx (via support) are exactly the outputs with nonzero probability in evalDist mx.

instance instEvalDistCompatibleSPMF : EvalDistCompatible SPMF

SPMF is trivially compatible: both lifts coincide on the nose.

@[reducible, inline]

def evalDist {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx : m α) : SPMF α

The resulting distribution of running the monadic computation mx.

def «term𝒟[_]» : Lean.ParserDescr

Evaluation distribution notation for any monad lifting into SPMF.

theorem evalDist_def {m : Type u → Type v} [MonadLiftT m SPMF] {α : Type u} (mx : m α) : 𝒟[mx] = liftM mx

def probOutput {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (x : α) : ENNReal

Probability that a computation mx returns the value x.

noncomputable def probEvent {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : α → Prop) : ENNReal

Probability that a computation mx outputs a value satisfying p.

def probFailure {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : ENNReal

Probability that a computation mx will fail to return a value.

def «termPr[=_|_]» : Lean.ParserDescr

Probability that a computation returns a particular output.

def probEventNotation : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

def «termPr[⊥|_]» : Lean.ParserDescr

Probability that a computation fails to return a value.

theorem probOutput_def {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (x : α) : Pr[= x | mx] = 𝒟[mx] x

theorem mem_support_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : x ∈ support mx ↔ Pr[= x | mx] ≠ 0

theorem mem_support_iff_evalDist_apply_ne_zero {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : x ∈ support mx ↔ 𝒟[mx] x ≠ 0

theorem mem_finSupport_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [DecidableEq α] [HasEvalFinset m] (mx : m α) (x : α) : x ∈ finSupport mx ↔ Pr[= x | mx] ≠ 0

theorem probOutput_ne_zero_of_mem_support {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {x : α} (h : x ∈ support mx) : Pr[= x | mx] ≠ 0

theorem probOutput_eq_zero_of_not_mem_support {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {x : α} (h : x ∉ support mx) : Pr[= x | mx] = 0

@[simp]

theorem probOutput_eq_zero_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : Pr[= x | mx] = 0 ↔ x ∉ support mx

theorem not_mem_support_of_probOutput_eq_zero {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : Pr[= x | mx] = 0 → x ∉ support mx

Alias of the forward direction of probOutput_eq_zero_iff.

theorem probOutput_eq_zero {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : x ∉ support mx → Pr[= x | mx] = 0

Alias of the reverse direction of probOutput_eq_zero_iff.

@[simp]

theorem zero_eq_probOutput_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : 0 = Pr[= x | mx] ↔ x ∉ support mx

theorem zero_eq_probOutput {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : x ∉ support mx → 0 = Pr[= x | mx]

Alias of the reverse direction of zero_eq_probOutput_iff.

@[simp]

theorem probOutput_eq_zero_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : Pr[= x | mx] = 0 ↔ x ∉ finSupport mx

theorem not_mem_fin_support_of_probOutput_eq_zero {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : Pr[= x | mx] = 0 → x ∉ finSupport mx

Alias of the forward direction of probOutput_eq_zero_iff'.

theorem probOutput_eq_zero' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : x ∉ finSupport mx → Pr[= x | mx] = 0

Alias of the reverse direction of probOutput_eq_zero_iff'.

@[simp]

theorem zero_eq_probOutput_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : 0 = Pr[= x | mx] ↔ x ∉ finSupport mx

theorem zero_eq_probOutput' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : x ∉ finSupport mx → 0 = Pr[= x | mx]

Alias of the reverse direction of zero_eq_probOutput_iff'.

@[simp]

theorem probOutput_pos_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : 0 < Pr[= x | mx] ↔ x ∈ support mx

theorem probOutput_pos {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : x ∈ support mx → 0 < Pr[= x | mx]

Alias of the reverse direction of probOutput_pos_iff.

theorem mem_support_of_probOutput_pos {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : 0 < Pr[= x | mx] → x ∈ support mx

Alias of the forward direction of probOutput_pos_iff.

@[simp]

theorem probOutput_pos_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : 0 < Pr[= x | mx] ↔ x ∈ finSupport mx

theorem mem_finSupport_of_probOutput_pos {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : 0 < Pr[= x | mx] → x ∈ finSupport mx

Alias of the forward direction of probOutput_pos_iff'.

theorem probOutput_pos' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] : x ∈ finSupport mx → 0 < Pr[= x | mx]

Alias of the reverse direction of probOutput_pos_iff'.

@[implicit_reducible]

instance decidablePred_probOutput_eq_zero {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [hm : HasEvalSet.Decidable m] (mx : m α) : DecidablePred fun (x : α) => Pr[= x | mx] = 0

theorem probOutput_ne_zero {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) (h : x ∈ support mx) : Pr[= x | mx] ≠ 0

theorem probOutput_ne_zero' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) [HasEvalFinset m] [DecidableEq α] (h : x ∈ finSupport mx) : Pr[= x | mx] ≠ 0

@[simp]

theorem support_probOutput {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) : Function.support (probOutput mx) = support mx

theorem probEvent_def {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : α → Prop) : probEvent mx p = (OptionT.run 𝒟[mx]).toOuterMeasure (some '' {x : α | p x})

theorem probEvent_eq_tsum_indicator {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : α → Prop) : probEvent mx p = ∑' (x : α), {x : α | p x}.indicator (fun (x : α) => Pr[= x | mx]) x

theorem probEvent_eq_sum_fintype_indicator {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [Fintype α] (mx : m α) (p : α → Prop) : probEvent mx p = ∑ x : α, {x : α | p x}.indicator (fun (x : α) => Pr[= x | mx]) x

theorem probEvent_eq_tsum_ite {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑' (x : α), if p x then Pr[= x | mx] else 0

theorem probEvent_eq_sum_fintype_ite {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [Fintype α] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑ x : α, if p x then Pr[= x | mx] else 0

theorem probEvent_eq_tsum_subtype {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : α → Prop) : probEvent mx p = ∑' (x : ↑{x : α | p x}), Pr[= ↑x | mx]

theorem probEvent_eq_sum_filter_univ {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [Fintype α] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑ x : α with p x, Pr[= x | mx]

@[simp]

theorem probEvent_eq_zero_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} : probEvent mx p = 0 ↔ ∀ x ∈ support mx, ¬p x

theorem probEvent_eq_zero {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} : (∀ x ∈ support mx, ¬p x) → probEvent mx p = 0

Alias of the reverse direction of probEvent_eq_zero_iff.

@[simp]

theorem probEvent_eq_zero_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : probEvent mx p = 0 ↔ ∀ x ∈ finSupport mx, ¬p x

theorem probEvent_eq_zero' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : (∀ x ∈ finSupport mx, ¬p x) → probEvent mx p = 0

Alias of the reverse direction of probEvent_eq_zero_iff'.

@[simp]

theorem probEvent_ne_zero_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} : probEvent mx p ≠ 0 ↔ ∃ x ∈ support mx, p x

theorem probEvent_ne_zero {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} : (∃ x ∈ support mx, p x) → probEvent mx p ≠ 0

Alias of the reverse direction of probEvent_ne_zero_iff.

@[simp]

theorem probEvent_ne_zero_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : probEvent mx p ≠ 0 ↔ ∃ x ∈ finSupport mx, p x

theorem probEvent_ne_zero' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : (∃ x ∈ finSupport mx, p x) → probEvent mx p ≠ 0

Alias of the reverse direction of probEvent_ne_zero_iff'.

@[simp]

theorem probEvent_pos_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} : 0 < probEvent mx p ↔ ∃ x ∈ support mx, p x

theorem probEvent_pos {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} : (∃ x ∈ support mx, p x) → 0 < probEvent mx p

Alias of the reverse direction of probEvent_pos_iff.

@[simp]

theorem probEvent_pos_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : 0 < probEvent mx p ↔ ∃ x ∈ finSupport mx, p x

theorem probEvent_pos' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p : α → Prop} [HasEvalFinset m] [DecidableEq α] : (∃ x ∈ finSupport mx, p x) → 0 < probEvent mx p

Alias of the reverse direction of probEvent_pos_iff'.

theorem probEvent_eq_tsum_subtype_mem_support {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (p : α → Prop) : probEvent mx p = ∑' (x : ↑{x : α | x ∈ support mx ∧ p x}), Pr[= ↑x | mx]

theorem probEvent_eq_tsum_subtype_support_ite {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑' (x : ↑(support mx)), if p ↑x then Pr[= ↑x | mx] else 0

theorem probEvent_eq_sum_filter_finSupport {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑ x ∈ finSupport mx with p x, Pr[= x | mx]

theorem probEvent_eq_sum_finSupport_ite {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (p : α → Prop) [DecidablePred p] : probEvent mx p = ∑ x ∈ finSupport mx, if p x then Pr[= x | mx] else 0

theorem probEvent_ext {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} {p q : α → Prop} (h : ∀ x ∈ support mx, p x ↔ q x) : probEvent mx p = probEvent mx q

If two events are equivalent on the support of mx then they have the same output chance.

@[simp]

theorem probEvent_eq_eq_probOutput {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (x : α) : (probEvent mx fun (x_1 : α) => x_1 = x) = Pr[= x | mx]

@[simp]

theorem probEvent_eq_eq_probOutput' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (x : α) : (probEvent mx fun (x_1 : α) => x = x_1) = Pr[= x | mx]

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

def probEventBinding1 : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate.

def probEventBinding2 : Lean.ParserDescr

Probability that a computation returns a value satisfying a predicate. See probOutput_true_eq_probEvent for relation to the above definitions.

@[simp]

theorem evalDist_cast {α β : Type u} {m : Type u → Type u_1} [Monad m] [MonadLiftT m SPMF] (h : α = β) (mx : m α) : 𝒟[cast ⋯ mx] = cast ⋯ 𝒟[mx]

theorem evalDist_ext {α : Type u} {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [MonadLiftT m SPMF] [Monad n] [MonadLiftT n SPMF] {mx : m α} {mx' : n α} (h : ∀ (x : α), Pr[= x | mx] = Pr[= x | mx']) : 𝒟[mx] = 𝒟[mx']

theorem evalDist_ext_iff {α : Type u} {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [MonadLiftT m SPMF] [Monad n] [MonadLiftT n SPMF] {mx : m α} {mx' : n α} : 𝒟[mx] = 𝒟[mx'] ↔ ∀ (x : α), Pr[= x | mx] = Pr[= x | mx']

@[simp]

theorem evalDist_eq_liftM_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : PMF α) : 𝒟[mx] = liftM p ↔ ∀ (x : α), Pr[= x | mx] = p x

@[simp]

theorem evalDist_eq_mk_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : PMF (Option α)) : 𝒟[mx] = SPMF.mk p ↔ ∀ (x : α), Pr[= x | mx] = p (some x)

theorem evalDist_eq_liftM {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : PMF α} (h : ∀ (x : α), Pr[= x | mx] = p x) : 𝒟[mx] = liftM p

@[simp]

theorem evalDist_apply_eq_zero_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : Option α) : (OptionT.run 𝒟[mx]) x = 0 ↔ Option.rec (Pr[⊥ | mx] = 0) (fun (x : α) => x ∉ support mx) x

@[simp]

theorem evalDist_apply_eq_zero_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] (mx : m α) (x : Option α) : (OptionT.run 𝒟[mx]) x = 0 ↔ Option.rec (Pr[⊥ | mx] = 0) (fun (x : α) => x ∉ finSupport mx) x

@[simp]

theorem evalDist_ite {m : Type u → Type v} {α : Type u} (p : Prop) [Decidable p] [MonadLiftT m SPMF] (mx mx' : m α) : 𝒟[if p then mx else mx'] = if p then 𝒟[mx] else 𝒟[mx']

@[simp]

theorem probOutput_ite {m : Type u → Type v} {α : Type u} (p : Prop) [Decidable p] [MonadLiftT m SPMF] (x : α) (mx mx' : m α) : Pr[= x | if p then mx else mx'] = if p then Pr[= x | mx] else Pr[= x | mx']

@[simp]

theorem probFailure_ite {m : Type u → Type v} {α : Type u} (p : Prop) [Decidable p] [MonadLiftT m SPMF] (mx mx' : m α) : Pr[⊥ | if p then mx else mx'] = if p then Pr[⊥ | mx] else Pr[⊥ | mx']

@[simp]

theorem probEvent_ite {m : Type u → Type v} {α : Type u} (p : Prop) [Decidable p] [MonadLiftT m SPMF] (mx mx' : m α) (q : α → Prop) : probEvent (if p then mx else mx') q = if p then probEvent mx q else probEvent mx' q

theorem evalDist_eqRec {m : Type u → Type v} {α β : Type u} [MonadLiftT m SPMF] (h : α = β) (mx : m α) : 𝒟[h ▸ mx] = h ▸ 𝒟[mx]

theorem probOutput_eqRec {m : Type u → Type v} {α β : Type u} [MonadLiftT m SPMF] (h : α = β) (mx : m α) (y : β) : Pr[= y | h ▸ mx] = Pr[= ⋯ ▸ y | mx]

@[simp]

theorem probFailure_eqRec {m : Type u → Type v} {α β : Type u} [MonadLiftT m SPMF] (h : α = β) (mx : m α) : Pr[⊥ | h ▸ mx] = Pr[⊥ | mx]

theorem probEvent_eqRec {m : Type u → Type v} {α β : Type u} [MonadLiftT m SPMF] (h : α = β) (mx : m α) (q : β → Prop) : probEvent (h ▸ mx) q = probEvent mx fun (x : α) => q (h ▸ x)

theorem probOutput_true_eq_probEvent {α : Type} {m : Type → Type u} [Monad m] [MonadLiftT m SPMF] [LawfulMonadLiftT m SPMF] (mx : m α) (p : α → Prop) : Pr[= True | do let x ← mx pure (p x)] = probEvent mx p

Connection between the two different probability notations.

@[simp]

theorem tsum_probOutput_add_probFailure {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : ∑' (x : α), Pr[= x | mx] + Pr[⊥ | mx] = 1

@[simp]

theorem probFailure_add_tsum_probOutput {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : Pr[⊥ | mx] + ∑' (x : α), Pr[= x | mx] = 1

@[simp]

theorem probOutput_le_one {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] : Pr[= x | mx] ≤ 1

@[simp]

theorem probOutput_ne_top {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] : Pr[= x | mx] ≠ ⊤

@[simp]

theorem probOutput_lt_top {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] : Pr[= x | mx] < ⊤

@[simp]

theorem not_one_lt_probOutput {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] : ¬1 < Pr[= x | mx]

@[simp]

theorem tsum_probOutput_le_one {m : Type u → Type v} {α : Type u} {mx : m α} [MonadLiftT m SPMF] : ∑' (x : α), Pr[= x | mx] ≤ 1

@[simp]

theorem tsum_probOutput_ne_top {m : Type u → Type v} {α : Type u} {mx : m α} [MonadLiftT m SPMF] : ∑' (x : α), Pr[= x | mx] ≠ ⊤

@[simp]

theorem probEvent_le_one {m : Type u → Type v} {α : Type u} {mx : m α} {p : α → Prop} [MonadLiftT m SPMF] : probEvent mx p ≤ 1

@[simp]

theorem probEvent_ne_top {m : Type u → Type v} {α : Type u} {mx : m α} {p : α → Prop} [MonadLiftT m SPMF] : probEvent mx p ≠ ⊤

@[simp]

theorem probEvent_lt_top {m : Type u → Type v} {α : Type u} {mx : m α} {p : α → Prop} [MonadLiftT m SPMF] : probEvent mx p < ⊤

@[simp]

theorem not_one_lt_probEvent {m : Type u → Type v} {α : Type u} {mx : m α} {p : α → Prop} [MonadLiftT m SPMF] : ¬1 < probEvent mx p

@[simp]

theorem probFailure_le_one {m : Type u → Type v} {α : Type u} {mx : m α} [MonadLiftT m SPMF] : Pr[⊥ | mx] ≤ 1

@[simp]

theorem probFailure_ne_top {m : Type u → Type v} {α : Type u} {mx : m α} [MonadLiftT m SPMF] : Pr[⊥ | mx] ≠ ⊤

@[simp]

theorem probFailure_lt_top {m : Type u → Type v} {α : Type u} {mx : m α} [MonadLiftT m SPMF] : Pr[⊥ | mx] < ⊤

@[simp]

theorem not_one_lt_probFailure {m : Type u → Type v} {α : Type u} {mx : m α} [MonadLiftT m SPMF] : ¬1 < Pr[⊥ | mx]

@[simp]

theorem one_le_probOutput_iff {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] : 1 ≤ Pr[= x | mx] ↔ Pr[= x | mx] = 1

@[simp]

theorem one_le_probEvent_iff {m : Type u → Type v} {α : Type u} {mx : m α} {p : α → Prop} [MonadLiftT m SPMF] : 1 ≤ probEvent mx p ↔ probEvent mx p = 1

@[simp]

theorem one_le_probFailure_iff {m : Type u → Type v} {α : Type u} {mx : m α} [MonadLiftT m SPMF] : 1 ≤ Pr[⊥ | mx] ↔ Pr[⊥ | mx] = 1

@[simp]

theorem probOutput_eq_one_iff {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] : Pr[= x | mx] = 1 ↔ Pr[⊥ | mx] = 0 ∧ support mx = {x}

theorem probOutput_eq_one {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] : Pr[⊥ | mx] = 0 ∧ support mx = {x} → Pr[= x | mx] = 1

Alias of the reverse direction of probOutput_eq_one_iff.

@[simp]

theorem one_eq_probOutput_iff {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] : 1 = Pr[= x | mx] ↔ Pr[⊥ | mx] = 0 ∧ support mx = {x}

theorem one_eq_probOutput {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] : Pr[⊥ | mx] = 0 ∧ support mx = {x} → 1 = Pr[= x | mx]

Alias of the reverse direction of one_eq_probOutput_iff.

@[simp]

theorem probOutput_eq_one_iff' {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] : Pr[= x | mx] = 1 ↔ Pr[⊥ | mx] = 0 ∧ finSupport mx = {x}

theorem probOutput_eq_one' {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] : Pr[⊥ | mx] = 0 ∧ finSupport mx = {x} → Pr[= x | mx] = 1

Alias of the reverse direction of probOutput_eq_one_iff'.

@[simp]

theorem one_eq_probOutput_iff' {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] : 1 = Pr[= x | mx] ↔ Pr[⊥ | mx] = 0 ∧ finSupport mx = {x}

theorem one_eq_probOutput' {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] : Pr[⊥ | mx] = 0 ∧ finSupport mx = {x} → 1 = Pr[= x | mx]

Alias of the reverse direction of one_eq_probOutput_iff'.

theorem probOutput_eq_one_of_support_subset_singleton {m : Type u → Type v} {α : Type u} {mx : m α} {x : α} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (hnf : Pr[⊥ | mx] = 0) (huniq : ∀ y ∈ support mx, y = x) : Pr[= x | mx] = 1

If a non-failing computation can only return x, then it returns x with probability one.

@[simp]

theorem probFailure_mul_le {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (r : ENNReal) : Pr[⊥ | mx] * r ≤ r

@[simp]

theorem mul_probFailure_le {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (r : ENNReal) : r * Pr[⊥ | mx] ≤ r

@[simp]

theorem probOutput_mul_le {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (r : ENNReal) (x : α) : Pr[= x | mx] * r ≤ r

@[simp]

theorem mul_probOutput_le {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (r : ENNReal) (x : α) : r * Pr[= x | mx] ≤ r

@[simp]

theorem probEvent_mul_le {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (r : ENNReal) (p : α → Prop) : probEvent mx p * r ≤ r

@[simp]

theorem mul_probEvent_le {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (r : ENNReal) (p : α → Prop) : r * probEvent mx p ≤ r

@[simp]

theorem tsum_probOutput_eq_sub {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : ∑' (x : α), Pr[= x | mx] = 1 - Pr[⊥ | mx]

theorem tsum_probOutput_eq_one' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} (h : Pr[⊥ | mx] = 0) : ∑' (x : α), Pr[= x | mx] = 1

@[simp]

theorem tsum_support_probOutput_eq_sub {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) : ∑' (x : ↑(support mx)), Pr[= ↑x | mx] = 1 - Pr[⊥ | mx]

theorem tsum_support_probOutput_eq_one' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} (h : Pr[⊥ | mx] = 0) : ∑' (x : ↑(support mx)), Pr[= ↑x | mx] = 1

@[simp]

theorem sum_probOutput_eq_sub {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [Fintype α] (mx : m α) : ∑ x : α, Pr[= x | mx] = 1 - Pr[⊥ | mx]

theorem sum_probOutput_eq_one {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [Fintype α] {mx : m α} (h : Pr[⊥ | mx] = 0) : ∑ x : α, Pr[= x | mx] = 1

@[simp]

theorem sum_finSupport_probOutput_eq_sub {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] (mx : m α) : ∑ x ∈ finSupport mx, Pr[= x | mx] = 1 - Pr[⊥ | mx]

theorem sum_finSupport_probOutput_eq_one {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] {mx : m α} (h : Pr[⊥ | mx] = 0) : ∑ x ∈ finSupport mx, Pr[= x | mx] = 1

theorem probFailure_eq_sub_tsum {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : Pr[⊥ | mx] = 1 - ∑' (x : α), Pr[= x | mx]

theorem probFailure_eq_sub_sum {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [Fintype α] (mx : m α) : Pr[⊥ | mx] = 1 - ∑ x : α, Pr[= x | mx]

@[simp]

theorem probEvent_False {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : (probEvent mx fun (x : α) => False) = 0

@[simp]

theorem probEvent_false {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : (probEvent mx fun (x : α) => false = true) = 0

@[simp]

theorem probEvent_True_eq_sub {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : (probEvent mx fun (x : α) => True) = 1 - Pr[⊥ | mx]

theorem probEvent_true_eq_sub {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : (probEvent mx fun (x : α) => true = true) = 1 - Pr[⊥ | mx]

theorem probFailure_eq_sub_probEvent {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : Pr[⊥ | mx] = 1 - probEvent mx fun (x : α) => True

theorem probFailure_eq_one_iff_probEvent_true {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) : Pr[⊥ | mx] = 1 ↔ (probEvent mx fun (x : α) => True) = 0

@[simp]

theorem probFailure_eq_one_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) : Pr[⊥ | mx] = 1 ↔ support mx = ∅

theorem probFailure_eq_one {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] {mx : m α} (h : support mx = ∅) : Pr[⊥ | mx] = 1

@[simp]

theorem probEvent_const {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : Prop) [Decidable p] : (probEvent mx fun (x : α) => p) = if p then 1 - Pr[⊥ | mx] else 0

Lemmas for monads with a total PMF denotation

These lemmas hold when m lifts into PMF (so computations never fail). They expose the absence of failure mass and total normalization of the resulting distribution.

@[simp]

theorem probFailure_of_liftM_PMF {α : Type u} {m : Type u → Type v} [MonadLiftT m PMF] (mx : m α) : Pr[⊥ | mx] = 0

A computation interpreted via a PMF lift has zero failure probability.

theorem tsum_probOutput_of_liftM_PMF {α : Type u} {m : Type u → Type v} [MonadLiftT m PMF] (mx : m α) : ∑' (x : α), Pr[= x | mx] = 1

theorem tsum_support_probOutput_of_liftM_PMF {α : Type u} {m : Type u → Type v} [MonadLiftT m PMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) : ∑' (x : ↑(support mx)), Pr[= ↑x | mx] = 1

theorem sum_probOutput_of_liftM_PMF {α : Type u} {m : Type u → Type v} [MonadLiftT m PMF] [Fintype α] (mx : m α) : ∑ x : α, Pr[= x | mx] = 1

theorem sum_finSupport_probOutput_of_liftM_PMF {α : Type u} {m : Type u → Type v} [MonadLiftT m PMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] (mx : m α) : ∑ x ∈ finSupport mx, Pr[= x | mx] = 1

theorem finSupport_nonempty_of_liftM_PMF {α : Type u} {m : Type u → Type v} [MonadLiftT m PMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] (mx : m α) : (finSupport mx).Nonempty

theorem probOutput_eq_inv_finSupport_card_of_liftM_PMF {α : Type u} {m : Type u → Type v} [MonadLiftT m PMF] [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] {mx : m α} {c : ENNReal} (hconst : ∀ x ∈ support mx, Pr[= x | mx] = c) : c = 1 / ↑(finSupport mx).card

theorem probEvent_compl {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p : α → Prop) : (probEvent mx p + probEvent mx fun (x : α) => ¬p x) = 1 - Pr[⊥ | mx]

theorem probEvent_or_le {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] (mx : m α) (p q : α → Prop) : (probEvent mx fun (x : α) => p x ∨ q x) ≤ probEvent mx p + probEvent mx q

Union bound: the probability of p ∨ q is at most the sum of probabilities.

theorem probEvent_mono {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p q : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] (h : ∀ x ∈ support mx, p x → q x) : probEvent mx p ≤ probEvent mx q

If p implies q on the support of a computation then it is more likely to happen.

theorem probEvent_mono' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p q : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] (h : ∀ x ∈ finSupport mx, p x → q x) : probEvent mx p ≤ probEvent mx q

If p implies q on the finSupport of a computation then it is more likely to happen.

theorem probEvent_mono'' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p q : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] (h : ∀ (x : α), p x → q x) : probEvent mx p ≤ probEvent mx q

If p implies q everywhere then p is less likely than q. Convenience specialisation of probEvent_mono that drops the support hypothesis.

@[simp]

theorem probEvent_eq_one_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] : probEvent mx p = 1 ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, p x

theorem probEvent_eq_one {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] : (Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, p x) → probEvent mx p = 1

Alias of the reverse direction of probEvent_eq_one_iff.

theorem probOutput_eq_one_iff_forall {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] (mx : m α) (x : α) : Pr[= x | mx] = 1 ↔ Pr[⊥ | mx] = 0 ∧ ∀ y ∈ support mx, y = x

Pointwise variant of probOutput_eq_one_iff: Pr[= x | mx] = 1 iff the support is a subset of {x} (phrased as a forall over the support) and the computation never fails.

More usable than probOutput_eq_one_iff when the caller wants to iterate over arbitrary support elements rather than prove a set equality.

@[simp]

theorem one_eq_probEvent_iff {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] : 1 = probEvent mx p ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, p x

theorem one_eq_probEvent {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] : (Pr[⊥ | mx] = 0 ∧ ∀ x ∈ support mx, p x) → 1 = probEvent mx p

Alias of the reverse direction of one_eq_probEvent_iff.

@[simp]

theorem probEvent_eq_one_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] : probEvent mx p = 1 ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ finSupport mx, p x

theorem probEvent_eq_one' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] : (Pr[⊥ | mx] = 0 ∧ ∀ x ∈ finSupport mx, p x) → probEvent mx p = 1

Alias of the reverse direction of probEvent_eq_one_iff'.

@[simp]

theorem one_eq_probEvent_iff' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] : 1 = probEvent mx p ↔ Pr[⊥ | mx] = 0 ∧ ∀ x ∈ finSupport mx, p x

theorem one_eq_probEvent' {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} {p : α → Prop} [MonadLiftT m SetM] [EvalDistCompatible m] [HasEvalFinset m] [DecidableEq α] : (Pr[⊥ | mx] = 0 ∧ ∀ x ∈ finSupport mx, p x) → 1 = probEvent mx p

Alias of the reverse direction of one_eq_probEvent_iff'.

@[simp]

theorem function_support_probOutput {m : Type u → Type v} {α : Type u} [MonadLiftT m SPMF] {mx : m α} [MonadLiftT m SetM] [EvalDistCompatible m] : (Function.support fun (x : α) => Pr[= x | mx]) = support mx

theorem mem_support_iff_of_evalDist_eq {α : Type u} {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [Monad n] [MonadLiftT n SPMF] [MonadLiftT n SetM] [EvalDistCompatible n] {mx : m α} {mx' : n α} (h : 𝒟[mx] = 𝒟[mx']) (x : α) : x ∈ support mx ↔ x ∈ support mx'

theorem mem_finSupport_iff_of_evalDist_eq {α : Type u} {m : Type u → Type u_1} {n : Type u → Type u_2} [Monad m] [MonadLiftT m SPMF] [MonadLiftT m SetM] [EvalDistCompatible m] [Monad n] [MonadLiftT n SPMF] [MonadLiftT n SetM] [EvalDistCompatible n] [HasEvalFinset m] [HasEvalFinset n] [DecidableEq α] {mx : m α} {mx' : n α} (h : 𝒟[mx] = 𝒟[mx']) (x : α) : x ∈ finSupport mx ↔ x ∈ finSupport mx'

theorem indicator_objective_eq_probEvent {m : Type u → Type v} {α β : Type u} [MonadLiftT m SPMF] (mx : m (α × β)) (R : α → β → Prop) : (∑' (z : α × β), Pr[= z | mx] * if R z.1 z.2 then 1 else 0) = probEvent mx fun (z : α × β) => R z.1 z.2