Lax Lean Archive

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

Characterisation of the slow space

Lax606786.SlowSpaceCharacterisation · concepts/Lax606786/SlowSpaceCharacterisation.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 cocycle, EE a fast space of multiplicity mm at rate λ\lambda, and λ′<λ\lambda' < \lambda. Suppose PωP_\omega are idempotents with range V(ω)V(\omega) and kernel containing E(ω)E(\omega), where X=E(ω)⊕V(ω)X = E(\omega) \oplus V(\omega), and that 1nlog⁡∥Lω(n)Pω∥→λ′\frac1n \log \|\mathcal{L}^{(n)}_\omega P_\omega\| \to \lambda' almost surely. Then almost surely V(ω)V(\omega) is the set of vectors growing at rate at most λ′\lambda':

    V(ω)={x∈X:λ(ω,x)≤λ′}.V(\omega) = \{x \in X : \lambda(\omega, x) \le \lambda'\}.

    Compare Corollary 30 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 15 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.FastSpaces
    2
    3/-!
    4---
    5title: Characterisation of the slow space
    6type: theorem
    7---
    8Let L\mathcal{L} be a cocycle, EE a fast space of multiplicity mm at rate λ\lambda, and
    9λ′<λ\lambda' < \lambda. Suppose PωP_\omega are idempotents with range V(ω)V(\omega) and kernel
    10containing E(ω)E(\omega), where X=E(ω)⊕V(ω)X = E(\omega) \oplus V(\omega), and that
    111nlog⁡∥Lω(n)Pω∥→λ′\frac1n \log \|\mathcal{L}^{(n)}_\omega P_\omega\| \to \lambda' almost surely. Then almost surely
    12V(ω)V(\omega) is the set of vectors growing at rate at most λ′\lambda':
    13V(ω)={x∈X:λ(ω,x)≤λ′}.V(\omega) = \{x \in X : \lambda(\omega, x) \le \lambda'\}.
    14Compare Corollary 30 of Lee (2024).
    15-/
    16
    17namespace Lax606786.SlowSpaceCharacterisation
    18
    19open MeasureTheory Filter
    20open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.FastSpaces Lax606786.ExtendedLog
    21
    22/-- The slow space is the set of vectors with growth rate at most the slow rate. -/
    23axiom V_characterisation {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    24 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    25 (R : Cocycle Ω X) {m : ℕ} [NeZero m] {lam : ℝ}
    26 {lam2 : EReal} (hgap : lam2 < lam) (E : Ω → GrassmannianFin X m) (hE : IsFastSpace R m lam E)
    27 (V : Ω → GrassmannianCofin X m) (P : Ω → X →L[ℝ] X)
    28 (hidem : ∀ᵐ ω ∂(R.μ), (P ω).comp (P ω) = P ω)
    29 (hcompl : ∀ᵐ ω ∂(R.μ), IsCompl ((E ω).1 : Submodule ℝ X) ((V ω).1.1 : Submodule ℝ X))
    30 (hPV : ∀ᵐ ω ∂(R.μ), LinearMap.range (P ω : X →ₗ[ℝ] X) = ((V ω).1.1 : Submodule ℝ X) ∧
    31 ∀ e ∈ ((E ω).1 : Submodule ℝ X), P ω e = 0)
    32 (hslow : ∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ =>
    33 logEReal ‖(R.iterate n ω).comp (P ω)‖ / (n : EReal)) atTop (nhds lam2)) :
    34 ∀ᵐ ω ∂(R.μ), (((V ω).1.1 : Submodule ℝ X) : Set X) = {x : X | R.lambdaAt ω x ≤ lam2}
    35
    36end Lax606786.SlowSpaceCharacterisation
    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…