Lax Lean Archive

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

Backward characterisation of the fast spaces

Lax606786.BackwardCharacterisation · concepts/Lax606786/BackwardCharacterisation.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, let (L,(λi),(mi),(Ei),(Vl),(Πl))(L, (\lambda_i), (m_i), (E_i), (V_l), (\Pi_l)) be an Oseledets decomposition of L\mathcal{L}, and let Bc(ω)B_c(\omega) be the set of vectors with a backward history at ω\omega decaying at rate cc. Then for every i<Li < L and almost every ω\omega,

    E1(ω)⊕⋯⊕Ei(ω)=Bλi(ω).E_1(\omega) \oplus \cdots \oplus E_i(\omega) = B_{\lambda_i}(\omega).

    In finite dimensions, and with an integrability assumption on the inverse, this is close to Lemma 20 of Froyland, Lloyd and Quas (2013). With zero-based indices the statement reads fastSumEiω=backwardSetRω(lami)fastSum E i ω = backwardSet R ω (lam i) for i+2≤Lvali + 2 ≤ Lval.

    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.OseledetsDecompositions
    3
    4/-!
    5---
    6title: Backward characterisation of the fast spaces
    7type: theorem
    8---
    9Let L\mathcal{L} be a cocycle on a separable Banach space XX, let
    10(L,(λi),(mi),(Ei),(Vl),(Πl))(L, (\lambda_i), (m_i), (E_i), (V_l), (\Pi_l)) be an Oseledets decomposition of L\mathcal{L},
    11and let Bc(ω)B_c(\omega) be the set of vectors with a backward history at ω\omega decaying at
    12rate cc. Then for every i<Li < L and almost every ω\omega,
    13E1(ω)⊕⋯⊕Ei(ω)=Bλi(ω).E_1(\omega) \oplus \cdots \oplus E_i(\omega) = B_{\lambda_i}(\omega).
    14In finite dimensions, and with an integrability assumption on the inverse, this is close to
    15Lemma 20 of Froyland, Lloyd and Quas (2013).
    16With zero-based indices the statement reads
    17`fastSum E i ω = backwardSet R ω (lam i)` for `i + 2 ≤ Lval`.
    18-/
    19
    20namespace Lax606786.BackwardCharacterisation
    21
    22open MeasureTheory Filter TopologicalSpace
    23open Lax606786.Grassmannian Lax606786.Cocycles Lax606786.OseledetsDecompositions
    24 Lax606786.BackwardHistories
    25
    26/-- The sum of the first `i + 1` fast spaces is the set of vectors with a backward history
    27decaying at rate `λ_{i+1}` (`lam i`). -/
    28axiom fastSum_eq_backwardSet {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    29 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    30 (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] [CompleteSpace X]
    31 {Lval : ℕ∞} {lam : ℕ → EReal} {mdim : ℕ → ℕ}
    32 {E : ∀ i : ℕ, ((i + 2 : ℕ) : ℕ∞) ≤ Lval → Ω → GrassmannianFin X (mdim i + 1)}
    33 {V : ℕ → Ω → Submodule ℝ X} {P : ℕ → Ω → X →L[ℝ] X}
    34 (h : IsOseledetsDecomposition R Lval lam mdim E V P)
    35 (i : ℕ) (hi : ((i + 2 : ℕ) : ℕ∞) ≤ Lval) :
    36 ∀ᵐ ω ∂(R.μ), (fastSum E i ω : Set X) = backwardSet R ω (lam i)
    37
    38end Lax606786.BackwardCharacterisation
    39
    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…