Definitions of a probability space

Probability measure

DefinitionEvents #

MeasurableSet s means that s is measurable (in the ambient measure space on α)

MeasurableSet.{u_1} {α : Type u_1} [MeasurableSpace α] (s : Set α) : Prop

Sources

MathlibMeasurableSet

Uses 1 · Used by 5

Statement usesSigma-algebra

Used byMeasurable function · Positive measure · Stopping time · Hahn decomposition theorem · Product of sigma-algebras

TheoremBorel-Cantelli lemma (easy direction)#

One direction of the Borel-Cantelli lemma (sometimes called the "first Borel-Cantelli lemma"): if (s i) is a sequence of sets such that ∑' i, μ (s i) is finite, then the limit superior of the s i along the atTop filter is a null set.

Note: for the second Borel-Cantelli lemma (applying to independent sets in a probability space), see ProbabilityTheory.measure_limsup_eq_one.

MeasureTheory.measure_limsup_atTop_eq_zero.{u_1, u_3} {α : Type u_1} {F : Type u_3}
  [FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F} {s : ℕ → Set α}
  (hs : ∑' (i : ℕ), μ (s i) ≠ ⊤) : μ (Filter.limsup s Filter.atTop) = 0

Sources

MathlibMeasureTheory.measure_limsup_atTop_eq_zero

Uses 3 · Used by 2

Statement usesInfinite sum · Real number

Proof usesOrder topology

Used byStrong law of large numbers · Vitali convergence theorem

TheoremBorel-Cantelli lemma (difficult direction)#

The second Borel-Cantelli lemma: Given a sequence of independent sets (sₙ) such that ∑ n, μ sₙ = ∞, limsup sₙ has measure 1.

ProbabilityTheory.measure_limsup_eq_one.{u_1} {Ω : Type u_1} {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} {s : ℕ → Set Ω} (hsm : ∀ (n : ℕ), MeasurableSet (s n))
  (hs : ProbabilityTheory.iIndepSet s μ) (hs' : ∑' (n : ℕ), μ (s n) = ⊤) :
  μ (Filter.limsup s Filter.atTop) = 1