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

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

Lax606786.OseledetsCompactnessCriterion · concepts/Lax606786/OseledetsCompactnessCriterion.lean · lax-606786

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let L\mathcal{L} be a cocycle on a separable Banach space XX, and suppose the growth rate of the compactness seminorm of its iterates is almost everywhere a constant κ\kappa:

    lim⁡n1nlog⁡∥Lω(n)∥c=κfor a.e. ω.\lim_n \tfrac1n \log \|\mathcal{L}^{(n)}_\omega\|_c = \kappa \quad \text{for a.e. } \omega.

    Then for any Oseledets decomposition (L,(λi),…)(L, (\lambda_i), \ldots) of L\mathcal{L}, the top exponent λ1=lim⁡n1nlog⁡∥Lω(n)∥\lambda_1 = \lim_n \frac1n \log\|\mathcal{L}^{(n)}_\omega\| satisfies κ≤λ1\kappa \le \lambda_1, and the decomposition is nontrivial (L≥2L \ge 2) exactly when κ≠λ1\kappa \ne \lambda_1. This is the last clause of Theorem 3 of Lee (2024), with the index of compactness in place of ν\nu. Such a κ\kappa always exists, by the concept IndexOfCompactnessIndexOfCompactness (existscompactnessIndexexists_compactnessIndex).

    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Lean source view on GitLab

    1import Lax606786.OseledetsDecompositions
    2
    3/-!
    4---
    5title: The Oseledets decomposition is nontrivial exactly when the compactness growth rate is smaller
    6type: theorem
    7---
    8Let L\mathcal{L} be a cocycle on a separable Banach space XX, and suppose the growth rate of the
    9compactness seminorm of its iterates is almost everywhere a constant κ\kappa:
    10lim⁡n1nlog⁡∥Lω(n)∥c=κfor a.e. ω.\lim_n \tfrac1n \log \|\mathcal{L}^{(n)}_\omega\|_c = \kappa \quad \text{for a.e. } \omega.
    11Then for any Oseledets decomposition (L,(λi),…)(L, (\lambda_i), \ldots) of L\mathcal{L}, the top exponent
    12λ1=lim⁡n1nlog⁡∥Lω(n)∥\lambda_1 = \lim_n \frac1n \log\|\mathcal{L}^{(n)}_\omega\| satisfies κ≤λ1\kappa \le \lambda_1, and
    13the decomposition is nontrivial (L≥2L \ge 2) exactly when κ≠λ1\kappa \ne \lambda_1. This is the last
    14clause of Theorem 3 of Lee (2024), with the index of compactness in place of ν\nu.
    15Such a κ\kappa always exists, by the concept `IndexOfCompactness` (`exists_compactnessIndex`).
    16-/
    17
    18namespace Lax606786.OseledetsCompactnessCriterion
    19
    20open MeasureTheory Filter TopologicalSpace
    21open Lax606786.BanachGrassmannian Lax606786.OperatorStatistics Lax606786.ExtendedLog
    22 Lax606786.Cocycles Lax606786.OseledetsDecompositions
    23
    24/-- `κ ≤ λ₁`, and `L ≥ 2` exactly when `κ ≠ λ₁`. -/
    25axiom kappa_le_and_two_le_iff {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    26 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    27 (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X]
    28 (κ : EReal) (hκ : ∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ =>
    29 logEReal (compactSeminorm (R.iterate n ω)) / (n : EReal)) atTop (nhds κ))
    30 {L : ℕ∞} {lam : ℕ → EReal} {m : ℕ → ℕ+}
    31 {E : ∀ i : ℕ, 1 ≤ i → (i : ℕ∞) < L → Ω → GrassmannianFin X (m i)}
    32 {V : ℕ → Ω → Submodule ℝ X} {P : ℕ → Ω → X →L[ℝ] X}
    33 (h : IsOseledetsDecomposition R L lam m E V P) :
    34 κ ≤ lam 1 ∧ ((2 : ℕ∞) ≤ L ↔ κ ≠ lam 1)
    35
    36end Lax606786.OseledetsCompactnessCriterion
    37
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…