While this submission is a draft, it cannot be used by other submissions.

Proof of `Backward characterisation of the fast spaces`

groundedproofs/Lax606786Proofs/Statements.lean · lax-606786

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.

Read the Lean proof on GitLab

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.