Theorems · Theorem

PMF.toOuterMeasure_bindOnSupport_apply

∀ {α : Type u_1} {β : Type u_2} {p : PMF α} (f : (a : α) → a ∈ p.support → PMF β) (s : Set β),
  (p.bindOnSupport f).toOuterMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s

Defined in

Mathlib.Probability.ProbabilityMassFunction.Monad

Cited by

1 results in Mathlib

Foundations

Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound