Let $\mathcal{L}$ be a cocycle on a separable Banach space $X$ over an invertible ergodic base $(\Omega, \sigma, \mu)$, and $(L, \lambda, m, E, V, \Pi)$ an Oseledets decomposition of it. Write $\zeta_n = \sigma^{-n}\omega$, so that $\mathcal{L}^{(n)}_{\zeta_n}$ carries the fibre over $\zeta_n$ forward to the fibre over $\omega$. Then for almost every $\omega$:

1. (fast spaces, from below) for $i < L$ and every real $a < \lambda_i$, eventually$$g\big(\mathcal{L}^{(n)}_{\zeta_n}, E_i(\zeta_n)\big) \ge e^{an};$$
2. (the whole space, from above) for every real $b > \lambda_1$, eventually $\|\mathcal{L}^{(n)}_{\zeta_n}\| \le e^{bn}$;
3. (slow spaces, from above) for $2 \le l \le L$ and every real $b > \lambda_l$, eventually $\|\mathcal{L}^{(n)}_{\zeta_n} v\| \le e^{bn}\|v\|$ for all $v \in V_l(\zeta_n)$.

These are the backward counterparts of the forward growth rates in the decomposition: the forward statements hold at a fixed base point as $n \to \infty$, whereas here the base point $\sigma^{-n}\omega$ moves with $n$.

In Lean, $\sigma^{-n}\omega$ is $(R.σ.symm : Ω → Ω)^[n] ω$.