Let $\mathcal{L}$ be a cocycle on a separable Banach space $X$, over an invertible ergodic base $(\Omega, \sigma, \mu)$. Let $\lambda_1 > \lambda_2 > \cdots$ be its distinct Lyapunov exponents, $m_i$ their multiplicities, and $L \in \{1, 2, \ldots, \infty\}$ the number of distinct exponents. Then $\lambda_i$ and $m_i$ are almost everywhere constant, $L \ge 2$ if and only if $\mathcal{L}$ is quasicompact, and there are

• measurable families of subspaces $E_i(\omega)$ of dimension $m_i$ (the fast spaces), for $i < L$,
• strongly measurable, tempered families of projections $\Pi_{l}(\omega)$, for $2 \le l \le L$, with ranges $V_l(\omega)$ (the slow spaces),

such that for almost every $\omega$:

1. $\mathcal{L}_\omega E_i(\omega) = E_i(\sigma\omega)$, and $E_i(\omega)$ grows at rate exactly $\lambda_i$, both in norm and in slowest growth:$$\lim_n \tfrac1n \log \|\mathcal{L}^{(n)}_\omega|_{E_i(\omega)}\| = \lim_n \tfrac1n \log g(\mathcal{L}^{(n)}_\omega, E_i(\omega)) = \lambda_i;$$
2. $X = E_1(\omega) \oplus \cdots \oplus E_{l-1}(\omega) \oplus V_l(\omega)$, and $\Pi_l(\omega)$ is the projection onto $V_l(\omega)$ along $E_1(\omega) \oplus \cdots \oplus E_{l-1}(\omega)$;
3. $\mathcal{L}_\omega V_l(\omega) \subseteq V_l(\sigma\omega)$;
4. $V_l(\omega) = \{x \in X : \lambda_\omega(x) \le \lambda_l\}$.

This is the semi-invertible form of Oseledets' multiplicative ergodic theorem (Oseledets 1968; Froyland, Lloyd and Quas 2013; González-Tokman and Quas 2014), for strongly measurable cocycles on separable Banach spaces as in Lee (2024). In other words, $\mathcal{L}$ has an Oseledets decomposition in the sense of the definition of Oseledets decompositions, whose zero-based indexing the Lean statement follows. Measurability of $E_i$ is with respect to the Borel structure of the Grassmannian; strong measurability of $\Pi_l$ means that $\omega \mapsto \Pi_l(\omega) x$ is measurable for each $x$.

Let $\sigma$ be an ergodic measure-preserving transformation of a probability space $(\Omega, \mu)$, and let $(f_n)$ be a subadditive family of integrable functions over $\sigma$. Then there is a constant $C \in [-\infty, \infty)$ such that

Limits are taken in the extended reals $[-\infty, \infty]$. The theorem is due to Kingman (1968).

Let $\sigma$ be an invertible ergodic measure-preserving transformation of a Lebesgue probability space $(\Omega, \mu)$ (a standard Borel space with a probability measure giving points measure zero), and let $(f_n)$ be a subadditive family of integrable functions over $\sigma$. Then the averages over the balanced time intervals $[-n, n)$ converge to the same constant as in Kingman's theorem:

with $C \in [-\infty, \infty)$ and limits taken in the extended reals. This is the balanced subadditive ergodic theorem of Lee (2024).

Let $\mathcal{L}$ be a cocycle on a separable Banach space $X$. If the growth rate of the compactness seminorm of the iterates exists and is almost everywhere equal to a constant $\kappa \in [-\infty, \infty]$,

then the index of compactness $\nu = \lim_k \chi_k$ equals $\kappa$ almost everywhere. This is the equivalence of growth statistics in the appendix of Lee (2024).

Let $\Omega = \{\pm1\}^{\mathbb{Z}}$ with its product $\sigma$-algebra, and let $X = \ell^1(\mathbb{Z})$. For $\omega \in \Omega$ let

Then $X$ is separable and every $V_\omega$ belongs to the Grassmannian $\mathcal{G} X$, but there is no measurable map $W : \Omega \to \mathcal{G} X$ with $W(\omega) = V_\omega$ for every $\omega \in \Omega$.

Over the shift $\sigma(\omega)_n = \omega_{n+1}$ with the Bernoulli measure, the operators $\mathcal{L}_\omega x = \varphi_\omega(x)\, e_0$ form a cocycle of rank one with $\lambda_1 = 0$, fast space $E_1(\omega) = \operatorname{span}\{e_0\}$ and slow space $V_\omega$; so separability of $X$ alone does not make the slow spaces measurable. This example is due to J. A. Horan (PhD thesis, University of Victoria, 2020). The argument: distinct $V_\omega$ are at distance at least $1$ in $\mathcal{G} X$ and $V_\omega = V_{-\omega}$, so a measurable $W$ would make every set $S = -S$ measurable, while there are more such sets than measurable ones.

In Lean a sign $\omega_i \in \{\pm1\}$ is coded by a boolean, $true$ for $+1$.