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

Fast spaces

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

definition

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

    Definition

    Let L\mathcal{L} be a cocycle on XX and λ∈R\lambda \in \mathbb{R}. A family E ⁣:Ω→GkXE \colon \Omega \to \mathcal{G}_k X of kk-dimensional subspaces is a fast space of multiplicity kk at rate λ\lambda when it is measurable and equivariant (LωE(ω)=E(σω)\mathcal{L}_\omega E(\omega) = E(\sigma\omega) almost surely), and almost surely every nonzero vector of E(ω)E(\omega) has growth rate λ\lambda and 1nlog⁡g(Lω(n),E(ω))→λ\tfrac1n \log g(\mathcal{L}^{(n)}_\omega, E(\omega)) \to \lambda.

    Concept map
    6 concepts; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitLab

    1import Lax606786.Cocycles
    2import Lax606786.BanachGrassmannian
    3import Lax606786.ExtendedLog
    4
    5/-!
    6---
    7title: Fast spaces
    8type: definition
    9---
    10Let L\mathcal{L} be a cocycle on XX and λ∈R\lambda \in \mathbb{R}. A family
    11E ⁣:Ω→GkXE \colon \Omega \to \mathcal{G}_k X of kk-dimensional subspaces is a *fast space* of
    12multiplicity kk at rate λ\lambda when it is measurable and equivariant
    13(LωE(ω)=E(σω)\mathcal{L}_\omega E(\omega) = E(\sigma\omega) almost surely), and almost surely every nonzero
    14vector of E(ω)E(\omega) has growth rate λ\lambda and
    151nlog⁡g(Lω(n),E(ω))→λ\tfrac1n \log g(\mathcal{L}^{(n)}_\omega, E(\omega)) \to \lambda.
    16-/
    17
    18namespace Lax606786.FastSpaces
    19
    20open MeasureTheory Filter
    21open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.OperatorStatistics
    22 Lax606786.ExtendedLog
    23
    24/-- `E` is a fast space of multiplicity `k` at rate `lam`. -/
    25def IsFastSpace {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    26 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    27 (R : Cocycle Ω X) (k : ℕ) [NeZero k] (lam : ℝ) (E : Ω → GrassmannianFin X k) : Prop :=
    28 Measurable E ∧
    29 (∀ᵐ ω ∂(R.μ), ∀ x ∈ (E ω).1, x ≠ 0 → R.lambdaAt ω x = (lam : EReal)) ∧
    30 (∀ᵐ ω ∂(R.μ), (E ω).1.map (R.L ω : X →ₗ[ℝ] X) = (E (R.σ ω)).1) ∧
    31 (∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ => logEReal (growth (R.iterate n ω) (E ω).1) / (n : EReal))
    32 atTop (nhds (lam : EReal)))
    33
    34end Lax606786.FastSpaces
    35

    Discussion

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

    Loading discussion…