Real-valued probabilities

Real-valued probabilities (μ a).toReal and (μ.toOuterMeasure s).toReal of a discrete distribution lie in [0, 1]. Nonnegativity is ENNReal.toReal_nonneg; this module supplies the upper bounds and monotonicity in the event, so that clients working with real-valued probabilities need not convert μ a ≤ 1, μ.toOuterMeasure s ≤ 1 or μ.toOuterMeasure s ≤ μ.toOuterMeasure t through ENNReal.toReal by hand.

Main results

• Cslib.Probability.PMF.toReal_apply_le_one: an outcome has real-valued probability at most one; in particular Pr[e] ≤ 1 for every Boolean experiment.
• Cslib.Probability.PMF.toOuterMeasure_toReal_le_one: an event has real-valued probability at most one. The name puts toOuterMeasure first, as the toOuterMeasure_toReal_* lemmas of CslibFrontier.Probability.PMF.Event do, rather than Mathlib's head-first toReal_toOuterMeasure_le_one.
• Cslib.Probability.PMF.toOuterMeasure_toReal_mono: a larger event has larger real-valued probability.

theorem Cslib.Probability.PMF.toReal_apply_le_one {α : Type u_1} (μ : PMF α) (a : α) : (μ a).toReal ≤ 1

A probability is at most one; in particular Pr[e] ≤ 1 for every Boolean experiment.

theorem Cslib.Probability.PMF.toOuterMeasure_toReal_le_one {α : Type u_1} (μ : PMF α) (s : Set α) : (μ.toOuterMeasure s).toReal ≤ 1

An event has real-valued probability at most one.

theorem Cslib.Probability.PMF.toOuterMeasure_toReal_mono {α : Type u_1} (μ : PMF α) {s t : Set α} (h : s ⊆ t) : (μ.toOuterMeasure s).toReal ≤ (μ.toOuterMeasure t).toReal

A larger event has larger real-valued probability. Unlike ENNReal.toReal_mono, this needs no finiteness side condition, since every event has probability at most one.