Event

In a probability space \((\Omega,\mathcal F,\mathbb P)\), a probability event is a measurable subset \(A\in\mathcal F\) of the sample space \(\Omega\). After an outcome \(\omega\in\Omega\) is specified, the statement that \(A\) occurs means exactly

This is a set-membership statement. It does not assert \(\mathbb P(A)\gt0\): in a continuous model, a nonempty event may have probability zero.

The logical types are different:

• an outcome is one element \(\omega\in\Omega\);
• an event is a yes-or-no question represented by a set of results; and
• a probability is mass assigned to that measurable set.

Start with a fair die

Roll a fair six-sided die. The outcome space is

and every face has probability \(1/6\). Give this finite space the collection of all subsets as its measurable sets, so every subset is an event.

Define two events:

and

If the die lands on \(4\), then the outcome is the single number \(4\). Both events occur because

The event \(A\) is not the outcome \(4\). It is the three-element set \(\{2,4,6\}\). The singleton \(\{4\}\) is yet another event, with probability \(1/6\).

Complement means “not”

The complement of \(A\), written \(A^{\mathsf c}\), contains every outcome in \(\Omega\) that is not in \(A\):

For any probability measure,

Here \(\mathbb P(A)=3/6=1/2\), so

Intersection means “and”

The intersection \(A\cap B\) contains outcomes that satisfy both questions:

There are two equally likely faces in the intersection, hence

The word “and” does not mean multiply probabilities automatically. The formula \(\mathbb P(A\cap B)=\mathbb P(A)\mathbb P(B)\) needs independence, which has not been assumed here. Indeed, its right-hand side would be \(1/4\), not the correct value \(1/3\).

Union means inclusive “or”

The union \(A\cup B\) contains outcomes that lie in \(A\), in \(B\), or in both:

It has probability

Adding \(\mathbb P(A)\) and \(\mathbb P(B)\) counts the overlap twice. The general two-event formula subtracts it once:

No independence hypothesis is needed for this inclusion-exclusion identity.

The exact definition and measurability gate

Let \(\Omega\) be an outcome space and let \(\mathcal F\) be a measurable collection of its subsets. An event is a set \(A\) satisfying

A probability measure \(\mathbb P\) then assigns \(A\) a number \(\mathbb P(A)\in[0,1]\). The collection \(\mathcal F\) contains the whole space and is closed under complements and countable unions. Consequently it is also closed under intersections and all the finite set operations used in the die example.

On a finite die, choosing every subset causes no trouble. On an uncountable space, probability theory usually selects a smaller measurable collection. There can be subsets outside that collection. They are still sets, but they are not events to which the probability model assigns an ordinary probability. The point is not to memorize a pathological example. It is to remember that “subset” and “measurable event” become different notions in general spaces.

Three special events

The whole space \(\Omega\) is the certain event and has probability one. The empty set \(\varnothing\) is the impossible event and has probability zero. A nonempty null event can also have probability zero in a continuous model, so zero probability and logical impossibility must not be identified.

For any event \(A\), these boundary identities hold:

In Lean: a set and its certificate are separate

Lean represents a subset of \(\Omega\) by Set Ω. It represents the measurability gate by a separate proposition and proof.

(A : Set Ω) (hA : MeasurableSet A)

The elementary set operations translate directly:

Mathlib’s measure object can be evaluated on an arbitrary Set Ω through its outer-measure foundation. The usual probability interpretation and exact measure identities are nevertheless stated with measurability gates where needed. A raw set term does not manufacture MeasurableSet A.

Small standalone tutorial: compute the die events

The set operations from the worked example can be checked without Mathlib. Here a Boolean predicate decides whether each face belongs to an event. Create /tmp/DieEvents.lean with these contents:

import Std

namespace DieEvents

def dieFaces : List Nat :=
  (List.range 6).map (fun k => k + 1)

def eventA (face : Nat) : Bool :=
  face % 2 == 0

def eventB (face : Nat) : Bool :=
  decide (4 ≤ face)

def select (P : Nat → Bool) : List Nat :=
  dieFaces.filter P

#eval select (fun face => !(eventA face))
#eval select (fun face => eventA face && eventB face)
#eval select (fun face => eventA face || eventB face)

example : select (fun face => !(eventA face)) = [1, 3, 5] := by decide
example : select (fun face => eventA face && eventB face) = [4, 6] := by decide
example : select (fun face => eventA face || eventB face) = [2, 4, 5, 6] := by
  decide

end DieEvents

From any directory on a normal macOS or Linux machine with the pinned compiler, type exactly:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean /tmp/DieEvents.lean

This exact worksheet was executed successfully with Lean 4.32.0 while repairing this page. It printed:

[1, 3, 5]
[4, 6]
[2, 4, 5, 6]

These are exactly \(A^{\mathsf c}\), \(A\cap B\), and \(A\cup B\) from the figure. Their lengths are \(3\), \(2\), and \(4\), so dividing by six gives the displayed probabilities \(1/2\), \(1/3\), and \(2/3\). This bounded tutorial imports only Std; it does not install the project’s Mathlib dependencies.

A real project event: convergence of orbit averages

The project does not reserve “event” for elementary experiments. In BirkhoffConvergence.lean, an outcome \(\omega\) is a starting point of a dynamical system. The event contains exactly those starting points whose finite Birkhoff averages converge to some real number.

This is the exact checked definition:

def birkhoffConvergenceSet (T : Ω → Ω) (g : Ω → ℝ) : Set Ω :=
  {ω | ∃ c : ℝ, Tendsto (fun n ↦ birkhoffAverage ℝ T g n ω) atTop (nhds c)}

Read the set-builder from left to right. The braces construct a set of starting points ω. Membership requires a real witness c and a proof that the average sequence tends to c. The definition does not claim that any starting point satisfies the property.

The same module separately proves the measurability gate:

theorem measurableSet_birkhoffConvergenceSet
    (hT : Measurable T) (hg : Measurable g) :
    MeasurableSet (birkhoffConvergenceSet T g) := by
  exact MeasureTheory.measurableSet_exists_tendsto
    (fun n ↦ measurable_birkhoffAverage hT hg n)

The event exists as a Set Ω without measurability assumptions. The theorem needs hT and hg to prove that it is a measurable event. This definition-theorem split is the general set-versus-event distinction made explicit in code.

import NonlinearDynamics.Random.RandomCocycles.BirkhoffConvergence

open MeasureTheory Set Filter
open NonlinearDynamics.Random.RandomCocycles

#check birkhoffConvergenceSet
#check mem_birkhoffConvergenceSet_iff
#check measurableSet_birkhoffConvergenceSet
#check preimage_birkhoffConvergenceSet

example {Ω : Type*} [MeasurableSpace Ω]
    (A B : Set Ω) (hA : MeasurableSet A) (hB : MeasurableSet B) :
    MeasurableSet (Aᶜ ∩ B) :=
  hA.compl.inter hB

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/BirkhoffConvergence.lean

Boundaries that prevent common mistakes

Where to continue

The measurable space entry explains the collection \(\mathcal F\) and why it is closed under the operations used here. The probability distribution (law) entry explains where probabilities on value-space events come from. The null set and almost-everywhere entries explain how zero-mass exceptions enter analysis.

For the project example, continue to the Birkhoff convergence event chapter and then to Birkhoff Convergence Events Before the Pointwise Ergodic Theorem. They separate event definition, measurability, invariance, zero-one rigidity, and actual convergence.

References

Olav Kallenberg. Foundations of Modern Probability, third edition, Springer, 2021. This is a standard reference for sample spaces, events, sigma algebras, and probability measures.

Mathlib contributors. Measurable spaces and measurable sets, Mathlib 4 documentation. This official reference documents MeasurableSet and its closure operations.

Project source. BirkhoffConvergence.lean contains the checked convergence-set definition and measurability theorem used in the Lean section.