Proof of `Backward characterisation of the fast spaces`
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Vectors of the fast spaces have backward histories decaying at the required rate; conversely, the slow component of a vector with such a history also has one, and vanishes. The backward growth bound on the fast spaces is a density argument in the manner of Mañé's lemma on tempered functions (Mañé 1983; González-Tokman and Quas 2015, Lemma 15). Froyland, Lloyd and Quas (2013, Lemma 20) obtain the corresponding bound in finite dimensions by assuming integrability of the inverse on the fast spaces, which is not needed here.