Lax Lean Archive

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

The exponents of an Oseledets decomposition

Lax606786.DecompositionExponents · concepts/Lax606786/DecompositionExponents.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 real normed space and (L,λ,m,E,V,Π)(L, \lambda, m, E, V, \Pi) an Oseledets decomposition of it. Then the exponents strictly decrease, λ1>λ2>⋯>λL\lambda_1 > \lambda_2 > \cdots > \lambda_L, the top exponent satisfies λ1<∞\lambda_1 < \infty, and every exponent λi\lambda_i with i<Li < L (one carrying a fast space) is a real number. Only the last exponent λL\lambda_L may be −∞-\infty.

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

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 lam_le_lam_one proven

    2 lam_ne_bot_ne_top proven

    3 lam_one_lt_top proven

    4 lam_succ_lt proven

    Lean source view on GitLab

    1import Lax606786.OseledetsDecompositions
    2
    3/-!
    4---
    5title: The exponents of an Oseledets decomposition
    6type: theorem
    7---
    8Let L\mathcal{L} be a cocycle on a real normed space and (L,λ,m,E,V,Π)(L, \lambda, m, E, V, \Pi) an
    9Oseledets decomposition of it. Then the exponents strictly decrease,
    10λ1>λ2>⋯>λL\lambda_1 > \lambda_2 > \cdots > \lambda_L, the top exponent satisfies λ1<∞\lambda_1 < \infty, and
    11every exponent λi\lambda_i with i<Li < L (one carrying a fast space) is a real number. Only the last
    12exponent λL\lambda_L may be −∞-\infty.
    13
    14-/
    15
    16namespace Lax606786.DecompositionExponents
    17
    18open TopologicalSpace
    19open Lax606786.BanachGrassmannian Lax606786.Cocycles Lax606786.OseledetsDecompositions
    20
    21variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    22 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    23 {R : Cocycle Ω X} {L : ℕ∞} {lam : ℕ → EReal} {m : ℕ → ℕ+}
    24 {E : ∀ i : ℕ, 1 ≤ i → (i : ℕ∞) < L → Ω → GrassmannianFin X (m i)}
    25 {V : ℕ → Ω → Submodule ℝ X} {P : ℕ → Ω → X →L[ℝ] X}
    26
    27/-- The exponents strictly decrease. -/
    28axiom lam_succ_lt (h : IsOseledetsDecomposition R L lam m E V P) {l : ℕ}
    29 (hl₁ : 1 ≤ l) (hl₂ : ((l + 1 : ℕ) : ℕ∞) ≤ L) : lam (l + 1) < lam l
    30
    31/-- Every exponent is at most the top one. -/
    32axiom lam_le_lam_one (h : IsOseledetsDecomposition R L lam m E V P) {l : ℕ}
    33 (hl₁ : 1 ≤ l) (hl₂ : (l : ℕ∞) ≤ L) : lam l ≤ lam 1
    34
    35/-- The top exponent is less than `∞`. -/
    36axiom lam_one_lt_top (h : IsOseledetsDecomposition R L lam m E V P) : lam 1 < ⊤
    37
    38/-- An exponent carrying a fast space is finite. -/
    39axiom lam_ne_bot_ne_top (h : IsOseledetsDecomposition R L lam m E V P) {l : ℕ}
    40 (hl₁ : 1 ≤ l) (hl₂ : (l : ℕ∞) < L) : lam l ≠ ⊥ ∧ lam l ≠ ⊤
    41
    42end Lax606786.DecompositionExponents
    43
    Show ProofShow ProofShow ProofShow 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…