Start with a space containing exactly two atoms, \(p\) and \(q\). An atom here is one indivisible outcome to which a measure assigns a weight. Give the atoms weights

\[ \mu(\{p\})=2, \qquad \mu(\{q\})=1, \]

and let the real-valued observable \(f\) report

\[ f(p)=1, \qquad f(q)=4. \]

There are two ledgers to add. The mass ledger adds the weights:

\[ \mu(\{p,q\})=2+1=3. \]

The integral ledger multiplies each value by its weight before adding:

\[ \int_{\{p,q\}} f\,d\mu {} = 2\cdot 1+1\cdot 4 {} = 2+4 {} = 6. \]

The normalized space average is the integral divided by total mass:

\[ \operatorname{Avg}_{\mu}(f) {} = \frac{6}{3} {} = 2. \]

The answer is not the unweighted average \((1+4)/2=5/2\). Atom \(p\) carries twice as much mass as atom \(q\), so its value \(1\) receives twice the weight.

Now multiply both atom weights by \(5\). The new measure \(5\mu\) has weights \(10\) and \(5\). Its two ledgers become

\[ \begin{aligned} (5\mu)(\{p,q\}) &=10+5=15,\\ \int_{\{p,q\}} f\,d(5\mu) &=10\cdot1+5\cdot4=10+20=30. \end{aligned} \]

Both numerator and denominator grew by \(5\), so their ratio did not:

\[ \operatorname{Avg}_{5\mu}(f)=\frac{30}{15}=2. \]

Finally, divide the original weights by their total mass \(3\). The resulting weights \(2/3\) and \(1/3\) add to \(1\), so they define a probability measure \(\widehat\mu\). Its ordinary integral is

\[ \int f\,d\widehat\mu {} = \frac23\cdot1+\frac13\cdot4 {} = \frac23+\frac43 {} = 2. \]

For a probability measure, this integral is also called the expectation of \(f\).

The original two atoms contribute two and four to an integral of six over mass three. Fivefold scaling changes their contributions to ten and twenty, giving integral thirty over mass fifteen. Probability normalization changes their weights to two thirds and one third, and all three routes give average two.
FigureThe complete two-atom ledger: \(p\) has value \(1\) and original weight \(2\), while \(q\) has value \(4\) and original weight \(1\). Thus the mass is \(2+1=3\), the integral is \(2\cdot1+1\cdot4=6\), and the normalized average is \(6/3=2\). Multiplying both weights by \(5\) gives weights \(10,5\), contributions \(10,20\), mass \(15\), integral \(30\), and the same ratio \(30/15=2\). Dividing the original weights by \(3\) instead gives probabilities \(2/3,1/3\), whose expectation is \(2/3+4/3=2\). These two rescalings illustrate the general cancellation of a common positive factor; they supply no orbit-average convergence result.

The general definition

Let \(\Omega\) be a space, let \(\mu\) assign mass to its measurable subsets, and let \(f:\Omega\to\mathbb R\) be an observable. Assume:

  • \(\mu\) is finite, meaning \(\mu(\Omega)\lt\infty\);
  • \(\mu\) is nonzero, meaning \(\mu(\Omega)\gt0\); and
  • \(f\) is integrable , meaning its absolute size has finite integral.

Then the normalized space average is

\[ \operatorname{Avg}_{\mu}(f) {} = \frac{1}{\mu(\Omega)}\int_{\Omega} f\,d\mu. \]

The measure tells us how much weight each part of the space receives. The integral adds the weighted values. Dividing by total mass converts that total into a per-unit-mass average.

If \(c\gt0\), then the scaled measure \(c\mu\) satisfies

\[ (c\mu)(\Omega)=c\mu(\Omega), \qquad \int f\,d(c\mu)=c\int f\,d\mu. \]

Therefore

\[ \operatorname{Avg}_{c\mu}(f) {} = \frac{c\int f\,d\mu}{c\mu(\Omega)} {} = \operatorname{Avg}_{\mu}(f). \]

This cancellation requires one common positive scale factor. Changing the relative weights can change the answer. For example, changing the two-atom weights from \((2,1)\) to \((1,2)\) gives

\[ \frac{1\cdot1+2\cdot4}{1+2}=\frac93=3, \]

not \(2\).

Why the denominator belongs in an ergodic theorem

Suppose a dynamical argument shows that a function is almost everywhere equal to a constant \(c\), and that its integral equals the integral of \(f\). Then

\[ \mu(\Omega)c=\int_{\Omega}f\,d\mu. \]

For finite nonzero mass, cancellation identifies

\[ c=\frac{1}{\mu(\Omega)}\int_{\Omega}f\,d\mu. \]

The denominator is not cosmetic. If \(\mu=2\delta_x\), twice the unit mass at one point \(x\), then

\[ \int h\,d\mu=2h(x), \qquad \operatorname{Avg}_{\mu}(h)=h(x). \]

The orbit samples only the value \(h(x)\), not the arbitrarily doubled raw integral. The project’s twenty-eighth Random Matrix Theory milestone (RMT-28) includes this mass-two boundary probe.

In Lean: write the average notation

Mathlib, Lean’s community mathematics library, uses a slashed integral sign for the normalized average.

One idea, three languages Read across, then read the syntax map
A human says
Take the integral of f with respect to mu, then normalize by the total mass of mu.
On paper
\(\operatorname{Avg}_{\mu}(f).\)
In Lean
⨍ x, f x ∂μ
Syntax map
  • ⨍ is Mathlib’s notation for an integral average, not an ordinary integral sign.
  • x is a bound variable ranging over the underlying space.
  • f x is the value contributed at \(x\).
  • ∂μ says that the measure is \(\mu\). The symbol after ∂ changes when the measure changes.
  • The notation elaborates to MeasureTheory.average μ f.

The notation is compact, but it hides the denominator. The next theorem makes that normalization explicit.

In Lean: expose the reciprocal mass

One idea, three languages Read across, then read the syntax map
A human says
The integral average equals the ordinary integral scaled by the reciprocal of the real total mass.
On paper
\(\operatorname{Avg}_{\mu}(f)=\bigl(\mu_{\mathbb R}(\Omega)\bigr)^{-1}\!\int_{\Omega}f\,d\mu.\)
In Lean
MeasureTheory.average_eq (μ := μ) f
Syntax map
  • average_eq is the exact Mathlib rewrite theorem.
  • (μ := μ) supplies the named measure argument explicitly.
  • In the theorem’s right-hand side, μ.real univ converts the total extended nonnegative mass to a real scalar. Here univ is the whole space \(\Omega\).
  • The postfix ⁻¹ is multiplicative inverse.
  • The operator • in the generic theorem is scalar multiplication. For real-valued \(f\), the project rewrites it as ordinary multiplication.
  • The equality is total and remains syntactically true in the fallback cases discussed below. It becomes the usual division formula only under the finite, nonzero, integrable interpretation.

The exact pinned generic theorem is

theorem MeasureTheory.average_eq (f : Ω → E) :
    ⨍ x, f x ∂μ = (μ.real Set.univ)⁻¹ • ∫ x, f x ∂μ

The codomain \(E\) may be more general than \(\mathbb R\); it is a normed additive commutative group with scalar multiplication by real numbers.

In Lean: probability mass one removes the denominator

One idea, three languages Read across, then read the syntax map
A human says
When mu is a probability measure, its total mass is one, so its normalized average is its ordinary integral.
On paper
\(\mu(\Omega)=1\quad\Longrightarrow\quad\operatorname{Avg}_{\mu}(f)=\int_{\Omega}f\,d\mu.\)
In Lean
MeasureTheory.average_eq_integral (μ := μ) f
Syntax map
  • average_eq_integral is a Mathlib theorem, not a new definition.
  • Its hidden typeclass premise [IsProbabilityMeasure μ] records \(\mu(\Omega)=1\).
  • ∫ x, f x ∂μ is the ordinary Bochner integral. Calling it an expectation is appropriate when \(\mu\) is a probability measure and \(f\) is the random variable under discussion.
  • The theorem itself is total; a mathematically informative expectation still needs the usual measurability and integrability conditions.

The exact pinned theorem is

theorem MeasureTheory.average_eq_integral
    [IsProbabilityMeasure μ] (f : Ω → E) :
    ⨍ x, f x ∂μ = ∫ x, f x ∂μ

In Lean: the project theorem adds dynamics

The normalized average is a static quantity. RMT-28 proves a separate theorem that identifies it as the limit of time averages under explicit dynamical hypotheses.

One idea, three languages Read across, then read the syntax map
A human says
On a finite nonzero ergodic measure-preserving system, the Birkhoff averages of an integrable real observable converge for almost every starting point to its normalized space average.
On paper
\(\mu\text{ finite},\ \mu\ne0,\ T\text{ ergodic},\ f\in L^1(\mu)\Longrightarrow \frac1n\sum_{j=0}^{n-1}f(T^j\omega)\to\frac{1}{\mu(\Omega)}\int f\,d\mu\text{ for }\mu\text{-almost every }\omega.\)
In Lean
ae_tendsto_birkhoffAverage_normalizedIntegral_of_ergodic (T := T) (f := f) hμ hT hf
Syntax map
  • hμ : μ ≠ 0 rules out zero total mass, while [IsFiniteMeasure μ] is an ambient instance ensuring finite mass.
  • hT : Ergodic T μ supplies both measure preservation and ergodic rigidity for the map \(T\).
  • hf : Integrable f μ is the analytic hypothesis on \(f\).
  • The theorem’s conclusion begins ∀ᵐ ω ∂μ, read “for almost every \(\omega\) with respect to \(\mu\).” It does not say every starting point.
  • Tendsto … atTop (nhds target) says the sequence converges as the natural-number horizon tends to infinity toward the displayed target.
  • birkhoffAverage ℝ T f n ω averages the first \(n\) observations along the orbit of \(\omega\).

Its exact declaration is

theorem ae_tendsto_birkhoffAverage_normalizedIntegral_of_ergodic
    [IsFiniteMeasure μ]
    (hμ : μ ≠ 0) (hT : Ergodic T μ) (hf : Integrable f μ) :
    ∀ᵐ ω ∂μ,
      Tendsto (fun n ↦ birkhoffAverage ℝ T f n ω) atTop
        (nhds ((μ.real univ)⁻¹ * ∫ x, f x ∂μ))

The theorem is stronger than the definition of an average and narrower than a general slogan about ergodicity: it is an almost-everywhere convergence result for integrable real observables under the exact listed assumptions.

A tiny standalone Lean worksheet a human can type

Standalone tutorial. This worksheet checks only the two finite integer ledgers. It does not import Mathlib, construct a measure, or prove an ergodic theorem.

Save the following as NormalizedAverageTutorial.lean:

import Std

inductive Atom where
  | p | q
deriving Repr, DecidableEq

def atoms : List Atom := [.p, .q]

def value : Atom → Nat
  | .p => 1
  | .q => 4

def originalWeight : Atom → Nat
  | .p => 2
  | .q => 1

def scaledWeight (scale : Nat) (x : Atom) : Nat :=
  scale * originalWeight x

def totalMass (weight : Atom → Nat) : Nat :=
  atoms.foldl (fun total x => total + weight x) 0

def weightedIntegral (weight : Atom → Nat) : Nat :=
  atoms.foldl (fun total x => total + weight x * value x) 0

def exactIntegerAverage (weight : Atom → Nat) : Nat :=
  weightedIntegral weight / totalMass weight

#eval [totalMass originalWeight,
       weightedIntegral originalWeight,
       exactIntegerAverage originalWeight]

#eval [totalMass (scaledWeight 5),
       weightedIntegral (scaledWeight 5),
       exactIntegerAverage (scaledWeight 5)]

example : totalMass originalWeight = 3 := by decide
example : weightedIntegral originalWeight = 6 := by decide
example : exactIntegerAverage originalWeight = 2 := by decide
example : totalMass (scaledWeight 5) = 15 := by decide
example : weightedIntegral (scaledWeight 5) = 30 := by decide
example : exactIntegerAverage (scaledWeight 5) = 2 := by decide

From the directory containing that file, type exactly:

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

The two output rows should be [3, 6, 2] and [15, 30, 2]. This command is suitable for an ordinary Mac or Linux machine because the worksheet imports only Std.

The tutorial uses natural-number division only because \(6/3\) and \(30/15\) are exact integers. It stores the probability weights \(2/3\) and \(1/3\) as the common numerator ledger \((2,1)\) over denominator \(3\). It is a check of the finite arithmetic, not an implementation of real integration or rational probability measures. This exact worksheet was executed successfully with the pinned Lean 4.32.0 compiler.

Try the exact declarations in the project

Try it in the repository NonlinearDynamics/Random/RandomCocycles/ErgodicBirkhoffLimit.lean

Full project check. This uses the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory. Create a temporary project query containing:

import NonlinearDynamics.Random.RandomCocycles.ErgodicBirkhoffLimit
import Mathlib.MeasureTheory.Integral.Average

open MeasureTheory Set Filter
open NonlinearDynamics.Random.RandomCocycles

#check MeasureTheory.average
#check MeasureTheory.average_eq
#check MeasureTheory.average_eq_integral
#check condExp_invariants_ae_eq_average_of_preErgodic
#check condExp_invariants_ae_eq_normalizedIntegral_of_preErgodic
#check ae_tendsto_birkhoffAverage_normalizedIntegral_of_ergodic
#check ae_tendsto_birkhoffAverage_integral_of_ergodic

Each #check asks the pinned elaborator for the exact declaration type. The full-project command below checks the authoritative RMT-28 source module, not the standalone worksheet. It uses the repository’s pinned Lean and Mathlib dependencies.

Full project check, from the repository root
cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/ErgodicBirkhoffLimit.lean

Resource note: this exact file uses the repository's pinned Lean and Mathlib dependencies. Initial project setup can require substantial disk space and build time. For a lightweight first step on macOS or Linux, use the page's standalone Lean-core or Std tutorial.

Totalized edge cases are conventions, not averages with evidence

Mathlib defines

noncomputable def MeasureTheory.average (μ : Measure Ω) (f : Ω → E) :=
  ∫ x, f x ∂(μ Set.univ)⁻¹ • μ

This is a total definition: Lean returns a value for every measure and function instead of leaving exceptional inputs undefined.

  • Zero measure. The scaled measure is again zero, and the average is zero. There is no positive mass over which to average.
  • Infinite total mass. The inverse of infinite extended mass is zero, so the normalized measure and average are zero. This is a library convention, not a claim that every infinite-volume mean physically equals zero.
  • Nonintegrable function. Mathlib’s totalized Bochner integral returns zero outside its integrable regime, so the average does too. That zero does not certify integrability and should not be interpreted as cancellation of positive and negative contributions.
  • Inverse of zero. In Lean’s field operations, the inverse of zero is defined to be zero. Thus average_eq remains a valid rewrite at zero mass, but the resulting identity has no ordinary division-by-positive- mass meaning.

These choices are valuable for algebraic rewriting because every expression has a type and a value. The semantic theorem in this page deliberately adds IsFiniteMeasure μ, μ ≠ 0, and Integrable f μ before identifying an ergodic limit with a genuine normalized average. The probability specialization supplies finite nonzero mass automatically but still keeps the observable’s integrability premise.

Space average is not time average

The normalized space average uses the measure over the whole state space. A time average follows one orbit:

\[ \frac1n\sum_{j=0}^{n-1}f(T^j\omega). \]

The two-atom arithmetic does not make these quantities equal. If \(T\) is the identity map, then a point starting at \(p\) reads \(1\) forever and a point starting at \(q\) reads \(4\) forever. Their time averages are \(1\) and \(4\), not the global normalized average \(2\). The identity map preserves the measure, but this two-positive-mass system is not ergodic .

RMT-27 first identifies the general Birkhoff limit as conditional expectation onto the invariant sigma algebra . RMT-28 adds ergodic rigidity, which makes that invariant target almost everywhere constant, and then the mass ledger identifies the constant as the normalized space average.

What this page does and does not establish

The two-atom calculation exhibits the particular rescaling

\[ (\text{mass},\text{integral})=(3,6) \quad\text{to}\quad (15,30) \]

while preserving the ratio \(2\). The general scaling identity follows by cancelling a common positive factor in both the integral and the total mass. More generally, the definition records a weighted average per unit mass.

It does not establish any of the following by definition alone:

  • that \(f\) is measurable or integrable;
  • that a totalized zero is a meaningful mean;
  • invariance under changing relative weights;
  • measure preservation or ergodicity of a map;
  • convergence of any orbit average;
  • convergence at every starting point;
  • a rate of convergence, mixing, independence, or decay of correlations;
  • a subadditive cocycle limit, Lyapunov exponent, or Oseledets splitting; or
  • an identity with normalized matrix trace without a separate theorem.

Where to continue

Ergodic Birkhoff Limits and Normalized Space Averages develops the conditional-expectation collapse and every RMT-28 assumption.

Birkhoff Limits, Invariant Sigma Algebras, and Conditional Expectation explains the nonergodic target that comes first.

The probability measure page derives the mass-one case. The expectation page explains when ordinary-integral language becomes probabilistic. The ergodic probability base page keeps probability normalization, measure preservation, ergodicity, and integrability as separate hypotheses.

References

Mathlib contributors. Integral averages, Mathlib 4.32.0 at pinned commit 81a5d257. This source is authoritative for ⨍, MeasureTheory.average, average_eq, average_eq_integral, and the documented totalized cases.

Nonlinear Dynamics in Lean contributors. ErgodicBirkhoffLimit.lean, the checked project source for the pre-ergodic conditional-expectation identification and the finite-measure and probability Birkhoff endpoints.