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$.