Expectation

For an integrable real-valued random variable \(X\), its expectation is the integral \(\int X\,d\mathbb P\). A nonnegative random variable also has an extended expectation, which may equal \(+\infty\). On a finite or countable discrete space, the integral is a probability-weighted sum over atoms. For an atomless real law, it is not a sum of “the probability of each exact value”: every singleton has probability zero. Expectation is not the result at one outcome, and it need not belong to the range \(X(\Omega)\).

Expectation is an integral with respect to a probability measure . The probability normalization matters: integrating the same quantity against a general measure of total mass \(2\) doubles the raw integral.

Start with three possible payoffs

Let the outcome space be

Define a real-valued payoff \(X\) and probability measure \(\mathbb P\) by

The three probabilities add to one:

Suppose one run produces \(\omega=M\). The realized payoff is then

That single observation does not erase the other possibilities. The law of \(X\) still assigns mass \(1/2\) to payoff \(-1\), mass \(1/3\) to payoff \(2\), and mass \(1/6\) to payoff \(5\). A realization is one selected value. In this finite example, the law is the complete weighted list of its three atoms.

Compute the weighted average exactly

On a finite probability space, expectation is the sum

For this payoff,

The negative payoff contributes \(-3/6\), while the two positive payoffs contribute \(4/6\) and \(5/6\). Expectation combines contributions; it does not choose the most likely payoff.

There is no outcome with payoff \(1\):

Thus an expectation need not be attainable in a single realization. It is the center of the probability-weighted values, not an additional attained value.

From a finite sum to an integral

For an integrable real random variable

on a probability space \((\Omega,\mathcal F,\mathbb P)\), expectation is

The sigma algebra \(\mathcal F\) specifies the measurable events , and \(\mathbb P\) assigns them probability. The function \(X\) must be measurable so that value-space questions pull back to events. Integrability ensures that the positive and negative contributions combine into a finite real number.

In the three-outcome example, the integral is exactly the weighted sum already computed. The integral notation is not a different average. It is the form that continues to work on continuous and mixed outcome spaces where listing all outcomes is impossible.

Expectation can also be computed from the law \(\mathcal L_{\mathbb P}(X)=X_*\mathbb P\):

The first integral averages over source outcomes. The second averages the identity function over the real value space. They agree because the law is the pushforward of \(\mathbb P\) through \(X\).

Raw mass is not probability expectation

Now define a new measure

Its atomic masses are \(1\), \(2/3\), and \(1/3\), and its total mass is

The raw integral scales with the measure:

This number is not the probability expectation of \(X\) under \(\nu\), because \(\nu\) is not a probability measure. If the intent is to turn a positive finite measure into a probability measure, normalization is an explicit operation:

The normalized average is then

Under a probability measure, the denominator is already one, so expectation is the raw integral. Under a mass-two measure, saying “expectation” without either normalizing or declaring a different convention hides a factor of two.

Linearity: transform first or average first

Expectation is linear. For integrable real random variables \(X\) and \(Z\) and real constants \(a\) and \(b\),

A constant function has expectation equal to that constant on a probability space. Therefore, if

then

The direct three-outcome calculation agrees. The transformed payoffs are \(1\), \(7\), and \(13\), so

Linearity does not say \(\mathbb E[XZ]=\mathbb E[X]\mathbb E[Z]\). That product identity requires additional assumptions such as independence and integrability of the product.

In Lean: type the integral that expectation names

∫ ω, X ω ∂μ

The project makes those two gates visible in its finite-horizon cocycle API:

C.finiteHorizonLogPlusExpectation hC k

The following definition and theorem are exact excerpts from the checked project source:

def finiteHorizonLogPlusExpectation [IsProbabilityMeasure μ]
    (C : DiscreteMatrixCocycle (ι := ι) μ)
    (_hC : C.HasIntegrableGeneratorLogPlus) (k : ℕ) : ℝ :=
  ∫ ω, C.logPlusNormObservable k ω ∂μ

@[simp] theorem finiteHorizonLogPlusExpectation_eq_integratedLogPlusNorm
    [IsProbabilityMeasure μ]
    {C : DiscreteMatrixCocycle (ι := ι) μ}
    (hC : C.HasIntegrableGeneratorLogPlus) (k : ℕ) :
    C.finiteHorizonLogPlusExpectation hC k = C.integratedLogPlusNorm k := by
  rfl

The underscore in _hC records that the proof is deliberately part of the interface even though the definition body does not compute with it. The equality proof is rfl: after unfolding the two project names, both sides are literally the same integral. The theorem is not a normalization formula. The probability typeclass has already required total mass one before the expectation name can be formed.

Try the three-payoff ledger locally

This first worksheet imports only Lean’s small Std library. It stores every probability as a numerator over the common denominator six, so the paper calculation

becomes exact integer arithmetic. Save this as /tmp/ExpectationScratch.lean on a normal Mac or Linux computer:

import Std

namespace ExpectationScratch

def payoffs : List Int := [-1, 2, 5]
def weightsSixths : List Nat := [3, 2, 1]

def contributionsSixths : List Int :=
  List.zipWith
    (fun payoff weight => payoff * Int.ofNat weight)
    payoffs weightsSixths

def totalSixths : Int :=
  contributionsSixths.foldl (fun total term => total + term) 0

def transformedPayoffs : List Int :=
  payoffs.map (fun payoff => 2 * payoff + 3)

def transformedContributionsSixths : List Int :=
  List.zipWith
    (fun payoff weight => payoff * Int.ofNat weight)
    transformedPayoffs weightsSixths

def transformedTotalSixths : Int :=
  transformedContributionsSixths.foldl (fun total term => total + term) 0

#eval contributionsSixths
#eval totalSixths
#eval totalSixths / 6
#eval transformedContributionsSixths
#eval transformedTotalSixths / 6

example : contributionsSixths = [-3, 4, 5] := by decide
example : totalSixths = 6 := by decide
example : totalSixths / 6 = 1 := by decide
example : transformedContributionsSixths = [3, 14, 13] := by decide
example : transformedTotalSixths / 6 = 5 := by decide

end ExpectationScratch

Type these two commands exactly:

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

This exact standalone worksheet was executed successfully with Lean 4.32.0. It printed:

[-3, 4, 5]
6
1
[3, 14, 13]
5

The three entries on the first line are the weighted contributions in sixths, not sampled payoffs. The proof lines ask Lean to check the same total and the linearity example \(Y=2X+3\). This bounded worksheet neither imports Mathlib nor constructs a measure-theoretic integral.

Full project check

The next worksheet uses the repository’s Mathlib-backed integral interface. Type it in a clone with the repository’s pinned Lean and Mathlib dependencies installed:

import NonlinearDynamics.Random.RandomCocycles.ProbabilityErgodicBase

open MeasureTheory

#check integral_add
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.finiteHorizonLogPlusExpectation
#check NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.finiteHorizonLogPlusExpectation_eq_integratedLogPlusNorm

variable {Ω : Type*} [MeasurableSpace Ω]
variable (μ : Measure Ω) (X Y : Ω → ℝ)

#check ∫ ω, X ω ∂μ

example (hX : Integrable X μ) (hY : Integrable Y μ) :
    (∫ ω, X ω + Y ω ∂μ) =
      (∫ ω, X ω ∂μ) + (∫ ω, Y ω ∂μ) := by
  exact integral_add hX hY

The first #check asks for Mathlib’s integral-linearity theorem. The next two inspect the project’s probability-normalized expectation definition and its equality with the raw integrated observable. The local variables make the line #check ∫ ω, X ω ∂μ meaningful. Finally, the example supplies explicit integrability proofs to integral_add, and Lean’s kernel checks the resulting additivity proof term. It is the typed counterpart of \(\mathbb E[X+Y]=\mathbb E[X]+\mathbb E[Y]\) when \(\mu\) is a probability measure, and a valid raw-integral identity for general \(\mu\).

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

Distinctions and failure modes

Where to continue

Read event for the measurable yes-or-no questions underlying the outcome space. Read measure and probability measure for the difference between raw mass and normalized mass. Read probability law for the value-space distribution that also determines expectation, and null set for changes that do not affect an integral.

The chapter Probability Normalization and Ergodic Rigidity Before Kingman places the project’s finite-horizon expectation beside its integrability and ergodicity assumptions.

References

Mathlib contributors. Bochner integral basics, Mathlib 4 documentation. This official implementation reference contains the real and vector-valued integral API, including integral_add and the integral of a constant.

Mathlib contributors. Probability measure typeclass, Mathlib 4 documentation. This official source records the total-mass-one assumption used by the project’s expectation interface.

Olav Kallenberg. Foundations of Modern Probability, third edition, Springer, 2021. This is a standard reference for expectation, integration, laws of random elements, and almost-everywhere equivalence.