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

Proof of `Slow vectors have no fast-decaying history`

groundedproofs/Lax606786Proofs/Backward.lean · lax-606786

What this proof establishes

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

A slow vector with a history decaying at rate λlλ_l would give the cocycle restricted to the slow space, modified to be bounded, a top exponent of at least λlλ_l along backward orbits. This contradicts Kingman's theorem along backward orbits (Lee 2024, Corollary 21), by which that top exponent is λl+1<λlλ_{l+1} < λ_l.