Proof of `Backward growth rates of the Oseledets spaces` (3rd statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Kingman's theorem for $σ⁻¹$ , applied to the norms of the iterates restricted to the slow spaces, whose forward rate is known uniformly.

Lax Lean Archive