Lax Lean Archive

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

Multiplicities of the Lyapunov exponents

Lax606786.MultiplicityFacts · concepts/Lax606786/MultiplicityFacts.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 and i≥1i \ge 1. If λi+1\lambda_{i+1} exists at ω\omega (that is, mi+1(ω)≠0m_{i+1}(\omega) \ne 0) then so does λi\lambda_i (mi(ω)≠0m_i(\omega) \ne 0); and L\mathcal{L} is quasicompact exactly when m1≠0m_1 \ne 0 almost everywhere.

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

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

    1 isQuasicompact_iff_mult_one proven

    2 mult_ne_zero_of_succ proven

    Lean source view on GitLab

    1import Lax606786.Cocycles
    2
    3/-!
    4---
    5title: Multiplicities of the Lyapunov exponents
    6type: theorem
    7---
    8Let L\mathcal{L} be a cocycle and i≥1i \ge 1. If λi+1\lambda_{i+1} exists at ω\omega (that is,
    9mi+1(ω)≠0m_{i+1}(\omega) \ne 0) then so does λi\lambda_i (mi(ω)≠0m_i(\omega) \ne 0); and L\mathcal{L} is
    10quasicompact exactly when m1≠0m_1 \ne 0 almost everywhere.
    11-/
    12
    13namespace Lax606786.MultiplicityFacts
    14
    15open MeasureTheory
    16open Lax606786.Cocycles
    17
    18variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    19 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    20
    21/-- A later multiplicity can be nonzero only if the earlier one is. -/
    22axiom mult_ne_zero_of_succ (R : Cocycle Ω X) (ω : Ω) {i : ℕ} (hi : 1 ≤ i)
    23 (h : R.mult (i + 1) ω ≠ 0) : R.mult i ω ≠ 0
    24
    25/-- Quasicompactness is `m_1 ≠ 0` almost everywhere. -/
    26axiom isQuasicompact_iff_mult_one (R : Cocycle Ω X) :
    27 R.IsQuasicompact ↔ ∀ᵐ ω ∂(R.μ), R.mult 1 ω ≠ 0
    28
    29end Lax606786.MultiplicityFacts
    30
    Show 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…