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

Proof of `Uniqueness of fast families below a spectral gap`

groundedproofs/Lax606786Proofs/Cocycle/FastSpace.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

The Grassmannian contraction estimate pushes E(σnω)E(σⁿω) and E′(σnω)E'(σⁿω) together, so their distance tends to 00 along every orbit; by measure preservation its distribution does not depend on nn, so it is 00 almost surely.