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

Quasicompactness in terms of the compactness seminorm

Lax606786.QuasicompactnessCriterion · concepts/Lax606786/QuasicompactnessCriterion.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 that

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

    for a constant κ∈[−∞,∞]\kappa \in [-\infty, \infty]. Then L\mathcal{L} is quasicompact if and only if κ<λ1\kappa < \lambda_1 almost everywhere. Combined with the Oseledets decomposition, the decomposition is nontrivial (L≥2L \ge 2) exactly when the growth rate of ∥Lω(n)∥c\|\mathcal{L}^{(n)}_\omega\|_c is strictly smaller than that of ∥Lω(n)∥\|\mathcal{L}^{(n)}_\omega\|.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitLab

    1import Lax606786.Cocycles
    2
    3/-!
    4---
    5title: Quasicompactness in terms of the compactness seminorm
    6type: theorem
    7---
    8Let L\mathcal{L} be a cocycle on a separable Banach space XX, and suppose that
    9lim⁡n1nlog⁡∥Lω(n)∥c=κfor a.e. ω\lim_n \tfrac1n \log \|\mathcal{L}^{(n)}_\omega\|_c = \kappa \quad \text{for a.e. } \omega
    10for a constant κ∈[−∞,∞]\kappa \in [-\infty, \infty]. Then L\mathcal{L} is quasicompact if and only if
    11κ<λ1\kappa < \lambda_1 almost everywhere. Combined with the Oseledets decomposition, the
    12decomposition is nontrivial (L≥2L \ge 2) exactly when the growth rate of
    13∥Lω(n)∥c\|\mathcal{L}^{(n)}_\omega\|_c is strictly smaller than that of ∥Lω(n)∥\|\mathcal{L}^{(n)}_\omega\|.
    14-/
    15
    16namespace Lax606786.QuasicompactnessCriterion
    17
    18open MeasureTheory Filter TopologicalSpace
    19open Lax606786.OperatorStatistics Lax606786.ExtendedLog Lax606786.Cocycles
    20
    21/-- Quasicompactness is `κ < λ₁`, for the growth rate `κ` of `‖𝓛^{(n)}_ω‖_c`. -/
    22axiom isQuasicompact_iff {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    23 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    24 (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X]
    25 (κ : EReal) (hκ : ∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ =>
    26 logEReal (compactSeminorm (R.iterate n ω)) / (n : EReal)) atTop (nhds κ)) :
    27 R.IsQuasicompact ↔ ∀ᵐ ω ∂(R.μ), κ < R.chi 1 ω
    28
    29end Lax606786.QuasicompactnessCriterion
    30
    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…