Lax Lean Archive

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

Slow vectors have no fast-decaying history

Lax606786.BackwardSlow · concepts/Lax606786/BackwardSlow.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 on a separable Banach space XX with its Borel σ\sigma-algebra, with distinct exponents λi\lambda_i almost surely, and let DD be a decomposition after the first ll fast spaces, with slow space VV. Then almost surely the only vector of V(ω)V(\omega) with a backward history decaying at rate λl\lambda_l is 00.

    Concept map
    8 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.BackwardHistories
    2import Lax606786.OseledetsLevels
    3
    4/-!
    5---
    6title: Slow vectors have no fast-decaying history
    7type: theorem
    8---
    9Let L\mathcal{L} be a cocycle on a separable Banach space XX with its Borel σ\sigma-algebra, with
    10distinct exponents λi\lambda_i almost surely, and let DD be a decomposition after the first
    11ll fast spaces, with slow space VV. Then almost surely the only vector of V(ω)V(\omega) with a
    12backward history decaying at rate λl\lambda_l is 00.
    13-/
    14
    15namespace Lax606786.BackwardSlow
    16
    17open MeasureTheory TopologicalSpace
    18open Lax606786.Cocycles Lax606786.OseledetsLevels Lax606786.BackwardHistories
    19
    20/-- The slow space meets the backward set of the current exponent only at `0`. -/
    21axiom eq_zero_of_mem_backwardSet {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    22 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    23 (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] {lam : ℕ → EReal}
    24 (hlam : ∀ i, ∀ᵐ ω ∂(R.μ), R.lambda i ω = lam i)
    25 {l : ℕ} {D : LevelData Ω X} (hD : IsLevel R lam l D) :
    26 ∀ᵐ ω ∂(R.μ), ∀ v ∈ ((D.V ω).1.1 : Submodule ℝ X), v ∈ backwardSet R ω (lam l) → v = 0
    27
    28end Lax606786.BackwardSlow
    29
    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…