Almost everywhere
A property holds almost everywhere when the set where it fails has measure zero, even if that exceptional set is not empty.
Knowledge Base / precise language
Glossary
A precise, searchable trail map for recurring terms in dynamics, analysis, probability, physics, and Lean.
Each entry gives you enough plain language to keep moving and enough precision to use the term correctly. Follow the cross-links when a definition depends on another idea, or continue into a Deep Dive when the concept deserves a full derivation.
Begin with one complete probability story
Suppose we roll a fair six-sided die and pay \(X=-1\) on an odd roll and \(X=2\) on an even roll. One tiny experiment already contains most of the vocabulary that later supports random matrices and ergodic theory:
- the six faces form the sample space;
- a collection of allowed questions forms the measurable space ;
- “the roll is even” is an event ;
- counting favorable faces gives a probability measure ;
- the payoff rule is a random variable ;
- its two output masses form its probability distribution ;
- its probability-weighted average is its expectation .
The diagram is a reading route, not merely a dependency chart. Each box names the concrete question answered by the corresponding chapter.
For a first pass, take this route:
- Measurable space → Event → Measure → Probability measure .
- Measurable function → Random variable → Pushforward measure → Probability distribution .
- Expectation → Integrability → Null set → Almost everywhere .
How every rebuilt chapter teaches
The revised entries deliberately repeat a dependable ascent:
- a small, exact example you can calculate by hand;
- a diagram that exposes the objects and arrows in that calculation;
- the general mathematical definition and the nearest tempting mistake;
- a bridge from an ordinary human sentence, to paper notation, to Lean syntax;
- a tiny standalone Lean worksheet that is safe to run locally;
- the exact repository import and
#checkcommands for the full formalization, labeled as full project checks when they require the pinned Lean and Mathlib dependencies.
You do not need to understand every Lean token on the first read. Type the tiny worksheet, change one value, observe what fails, and return to the syntax map. Full project checks need the repository’s pinned Lean and Mathlib dependencies and may require substantial disk space and memory. Learning Lean does not: the standalone tutorials run on ordinary macOS or Linux computers.
Where to go after probability
The main routes then branch:
- Random matrices: random matrix → Hermitian matrix → matrix trace → trace power → empirical spectra.
- Dynamics along an orbit: orbit and iterate → measure-preserving transformation → ergodicity → Birkhoff sum → convergence events.
- Deterministic stability: orbit and iterate → forward stability → basin of attraction → Lyapunov function → semiconjugacy and conjugacy , then bifurcation point .
- Random products: finite matrix products → cocycles → log-norm integrability → subadditive growth rates.
Those routes are being rebuilt in public. Every page marked Open working note is usable teaching material, but its visible review status still matters: publication is not a substitute for human mathematical review.
Basin of attraction
A basin of attraction is the set of initial states whose forward orbits converge to one point or approach one specified set.
Bifurcation point
A parameter where the reference whole-state-space conjugacy class is not locally constant; explicit invariant changes provide sufficient witnesses.
Birkhoff Cauchy exceptional set
A Birkhoff Cauchy exceptional set contains the starting points whose orbit-average sequence keeps separating by at least one fixed positive scale arbitrarily far into its tail.
Birkhoff convergence event
A Birkhoff convergence event collects exactly the starting points whose orbit averages approach a finite real limit; a four-state cycle makes the set concrete before pointwise, everywhere, and almost-everywhere claims are separated.
Birkhoff sum
A Birkhoff sum adds one observable along a finite orbit; in finite-block arguments, the orbit map is a power of the base map and the observable is one complete block cost.
Cartesian complex Gaussian law
A Cartesian complex Gaussian law joins two independent real Gaussian coordinates while keeping their means, component variances, total complex variance, and degenerate support visible.
Conditional expectation
Conditional expectation is the almost-everywhere unique integrable function visible to a chosen sub-sigma algebra that preserves the original function's integral on every event visible there.
Conjugate transpose
The conjugate transpose flips a complex matrix across its diagonal and conjugates every entry.
Continuous-time stability
Continuous-time forward stability uses one initial neighborhood to control nearby trajectories for every nonnegative real time.
Empirical spectral law
An empirical spectral law is the probability distribution of the empirical spectral measure produced by a random matrix, not the measure from one sample and not its average.
Empirical spectral measure
A finite matrix spectrum becomes a counting measure with multiplicity, then a probability-normalized empirical measure in positive dimension.
Ergodic probability base
An ergodic probability base has total mass one, preserves that measure under time evolution, and gives every invariant measurable event probability zero or one.
Ergodicity
Ergodicity means that measure-preserving dynamics have no measurable invariant region of intermediate mass, or equivalently no nonconstant measurable invariant information after null sets are ignored.
Event
A probability event is a measurable set of outcomes; it occurs when the realized outcome belongs to that set.
Expectation
Expectation is the probability-weighted average of a random quantity across its whole law, not the value of one realization.
Extended log-norm observable
The signed extended log of a cocycle norm records contraction, neutral size, expansion, and exact collapse without confusing any of them.
Finite matrix trace moment
A finite matrix trace moment is the expectation of a trace-power observable under a specified matrix law, after measurability, integrability, and normalization have each been made explicit.
Finite maximal ergodic inequality
Under a measure-preserving transformation, a finite maximal ergodic inequality says that an integrable observable has nonnegative integral over the points where one of its finite orbit sums becomes strictly positive, with a positive-threshold weak estimate for finite average-exceedance events on a finite measure space.
Finite orbit visit count
A finite orbit visit count adds zero-or-one membership tests along a fixed orbit prefix, before any normalization, limit, or recurrence claim is made.
Finite random-matrix product
A finite random-matrix product evaluates a finite time prefix at each outcome, multiplies the newest factor on the left, proves the resulting map measurable, and only then forms its pushforward law.
Forward matrix product
A forward matrix product composes a time-indexed sequence so the earliest factor acts first on a column vector, the newest factor is written on the left, and the empty horizon is the identity.
Forward stability
Forward stability means that every sufficiently close initial state remains uniformly close to one reference orbit for all natural-number times.
Gaussian distribution
A Gaussian distribution is the real probability law determined by a mean and a nonnegative variance, including a point mass when the variance is zero.
Gaussian unitary ensemble
The repository's finite Wigner-scaled GUE law, from independent Gaussian Hermitian coordinates through exact trace and normalized spectral moments.
Hermitian coordinate space
A minimal coordinate system for Hermitian matrices: real diagonal entries and complex strict-upper entries assemble the whole matrix without duplicated lower-triangle data.
Hermitian Frobenius geometry
Frobenius geometry turns Hermitian matrices into a real Euclidean space: diagonal coordinates count once, conjugate off-diagonal pairs count twice, and square-root-of-two scaling exposes orthonormal Gaussian coordinates.
Hermitian matrix
A Hermitian matrix equals its conjugate transpose, forcing real diagonal entries and conjugate-paired off-diagonal entries.
Independence
Independence says that every measurable joint event has the product of its marginal probabilities under a specified probability measure.
Independent Cartesian complex Gaussian family
An independent Cartesian complex Gaussian family is an indexed collection of measurable complex variables with explicit coordinate laws and one mutual-independence statement across the collection.
Induced infinity operator norm
The maximum absolute row sum is exactly the worst-case amplification factor for a finite vector's supremum norm.
Infinite-horizon Birkhoff-average exceedance event
The infinite-horizon Birkhoff-average exceedance event contains the starting points whose finite-time orbit average strictly crosses a chosen threshold at least once.
Integrability
Integrability means that a measurable quantity has finite total absolute size under the chosen measure; under probability, this is finite expected absolute value.
Integrable generator log tails
Integrable generator log tails require genuine one-step inverses and finite average budgets for both logarithmic expansion and logarithmic contraction.
Integrated log-positive growth rate
Under an explicit one-step integrability hypothesis, the integrated log-positive growth rate is the deterministic Fekete limit obtained by integrating each finite cocycle expansion envelope against a preserved raw measure and then normalizing over positive time.
Integrated real-log growth rate
The integrated real-log growth rate is the finite Fekete limit of normalized signed expected cocycle log norms under pointwise invertibility and integrable forward and inverse generator tails.
Invariant sigma algebra
An invariant sigma algebra keeps exactly the measurable yes-or-no questions whose answers survive one pullback through the dynamics.
Koopman coboundary
A Koopman coboundary is a one-step potential difference whose orbit sum cancels internally and leaves only its final and initial endpoint values.
Koopman operator
A Koopman operator follows a state forward and then reads an observable there, turning possibly nonlinear state dynamics into linear composition on functions.
Limit inferior
The limit inferior is the eventual lower edge of a sequence: the rising limit of its tail infima, with explicit boundedness gates for Mathlib's real-valued definition.
Limit superior
The limit superior discards every finite prefix and records the highest level a sequence can still approach arbitrarily late.
Log-positive integrability envelope
Log-positive growth clips contraction at zero, leaving a nonnegative finite-horizon observable that one integrable generator bound can control along every finite orbit.
Lyapunov function
A Lyapunov function is a scalar certificate whose sign, sublevels, and change along an orbit can establish stability or attraction when the required comparison hypotheses are explicit.
Matrix trace
The trace adds a finite square matrix's diagonal entries; for one linear operator, that sum is unchanged by a change of basis.
Measurable function
A measurable function pulls every allowed target event back to an allowed source event.
Measurable space
A measurable space specifies which subsets count as observable events and keeps that collection closed under logical combinations.
Measure
A measure assigns nonnegative mass to measurable events, gives the empty event mass zero, and adds masses across disjoint events.
Measure-preserving transformation
A measure-preserving transformation is measurable and leaves the entire measure unchanged, so every measurable event and its preimage have equal mass.
Normalization convention
A normalization convention records matrix scale, trace divisor, measure mass, and dimension policy so numerically related quantities are not silently identified.
Normalized Hermitian coordinates
Normalized Hermitian coordinates correct the factor of two carried by reflected off-diagonal entries, turning one real coordinate ledger into an exact Frobenius-isometric description of Hermitian matrices.
Normalized space average
A normalized space average divides an integrable observable's integral by a finite nonzero total mass, so multiplying every mass by the same positive factor does not change the answer.
Null set
A null set is a set that carries exactly zero mass under a specified measure, even when the set is not empty.
One-sided discrete matrix cocycle
A one-sided discrete matrix cocycle repeatedly evaluates one matrix generator along a forward base orbit, with later factors multiplying on the left.
Orbit and iterate
An iterate applies one map repeatedly, while a forward orbit is the sequence or set of states reached from one chosen starting point.
Orbit-majorant centering
Orbit-majorant centering subtracts the additive sum of one-step values along each orbit, producing a nonpositive subadditive remainder rather than a mean-zero random variable.
Ordered interval packing
Ordered interval packing encodes positive-length half-open natural intervals by successive gaps, making containment, chronological order, disjointness, abutment, exact covered cardinality, and finite marked-start coverage available by construction.
Phase averaging
Phase averaging adds one fixed-block estimate from every residue phase, reindexes the resulting rectangle as consecutive orbit starts, and divides only when the block length is positive.
Probability distribution (law)
A probability distribution, or law, is the pushforward probability measure induced by a random object on its measurable value space.
Probability measure
A probability measure is a measure whose total mass on the whole outcome space is exactly one.
Pushforward measure
A pushforward measure transports mass through a measurable function by measuring preimages in the original space.
Random matrix
A random matrix maps each outcome to one ordinary matrix; measurability and a probability law are distinct additional layers.
Random variable
A real random variable is a measurable function from outcomes to real values; its law records how source probability is distributed across those values.
Semiconjugacy and conjugacy
A semiconjugacy maps one update rule into another and may lose information; a conjugacy is an invertible coordinate change that identifies the two dynamics.
Trace-power observable
A trace-power observable adds the diagonal of a matrix power, equivalently sums powers of the eigenvalues, and becomes a spectral moment after its normalization is fixed.
Uniform integrability
Uniform integrability gives one family-wide bound that prevents integrable mass from escaping into smaller sets or larger value tails.
Unitary invariance
A matrix law is unitarily invariant when every fixed unitary change of basis leaves the entire probability distribution unchanged.
Upper semicontinuity
Upper semicontinuity means that nearby function values cannot remain substantially above the value at the limiting input; downward jumps may still occur.
Variance
Variance is the expected squared distance from a random variable to its mean.
Weak-type (1,1) maximal bound
A weak-type (1,1) maximal bound controls the measure of starting points where some orbit average exceeds a positive threshold by the integrable size of the observable divided by that threshold.
Weyl eigenvalue bound
A Weyl eigenvalue bound says that a small Hermitian matrix perturbation can move no ordered eigenvalue coordinate by more than a controlled matrix-norm budget.
No matching term yet. The notebook may still define it in context.