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

Proof of `The Oseledets decomposition is nontrivial exactly when the compactness growth rate is smaller`

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

κ=ν≤χ1=λ1κ = ν ≤ χ_1 = λ_1 by the identification of the index of compactness; then quasicompactness, κ<λ1κ < λ_1 by the quasicompactness criterion, is κ≠λ1κ ≠ λ_1.