Lax Lean Archive

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

Existence of the top fast space

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

proven

Loading review…

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 quasicompact cocycle on a separable Banach space XX with its Borel σ\sigma-algebra, whose top exponent is almost surely χ1=λ1∈R\chi_1 = \lambda_1 \in \mathbb{R}, with multiplicity m1m_1.

    Then there is a fast space E1E_1 of multiplicity m1m_1 at rate λ1\lambda_1, on which the growth of Lω(n)\mathcal{L}^{(n)}_\omega is eventually positive.

    This is Lemma 28 of Lee (2024).

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 10 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.FastSpaces
    2
    3/-!
    4---
    5title: Existence of the top fast space
    6type: theorem
    7---
    8Let L\mathcal{L} be a quasicompact cocycle on a separable Banach space XX with its Borel
    9σ\sigma-algebra, whose top exponent is almost surely χ1=λ1∈R\chi_1 = \lambda_1 \in \mathbb{R}, with
    10multiplicity m1m_1.
    11
    12Then there is a fast space E1E_1 of multiplicity m1m_1 at rate λ1\lambda_1, on which the growth of
    13Lω(n)\mathcal{L}^{(n)}_\omega is eventually positive.
    14
    15This is Lemma 28 of Lee (2024).
    16-/
    17
    18namespace Lax606786.TopFastSpace
    19
    20open MeasureTheory Filter TopologicalSpace
    21open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.OperatorStatistics Lax606786.FastSpaces
    22
    23variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    24 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    25
    26/-- The top fast space exists, with eventually positive growth. -/
    27axiom exists_topFastSpace (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X]
    28 [CompleteSpace X] (hqc : R.IsQuasicompact)
    29 (lam : ℝ) (hlam : ∀ᵐ ω ∂(R.μ), R.chi 1 ω = (lam : EReal)) :
    30 ∃ (m1 : ℕ) (_ : NeZero m1) (E : Ω → GrassmannianFin X m1),
    31 (∀ᵐ ω ∂(R.μ), R.mult 1 ω = m1) ∧ IsFastSpace R m1 lam E ∧
    32 ∀ᵐ ω ∂(R.μ), ∀ᶠ n : ℕ in atTop, 0 < growth (R.iterate n ω) ((E ω).1 : Submodule ℝ X)
    33
    34end Lax606786.TopFastSpace
    35
    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…