Lax Lean Archive

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

Measurability of iterates, and constancy of the Lyapunov exponents

Lax606786.CocycleBasics · concepts/Lax606786/CocycleBasics.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.

    • Each iterate is strongly measurable: ω↦Lω(n)x\omega \mapsto \mathcal{L}^{(n)}_\omega x is measurable for every nn and xx.
    • For every kk the exponent χk\chi_k is almost everywhere equal to a constant; so are the distinct exponents λi\lambda_i and their multiplicities mim_i.
    Concept map
    6 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 exists_chi_ae_eq proven

    2 exists_lambda_ae_eq proven

    3 exists_mult_ae_eq proven

    4 measurable_iterate_apply proven

    In the paper

    • page 9 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.Cocycles
    2
    3/-!
    4---
    5title: Measurability of iterates, and constancy of the Lyapunov exponents
    6type: theorem
    7---
    8Let L\mathcal{L} be a cocycle on a separable Banach space XX with its Borel σ\sigma-algebra.
    9
    10- Each iterate is strongly measurable: ω↦Lω(n)x\omega \mapsto \mathcal{L}^{(n)}_\omega x is measurable
    11 for every nn and xx.
    12- For every kk the exponent χk\chi_k is almost everywhere equal to a constant; so are the
    13 distinct exponents λi\lambda_i and their multiplicities mim_i.
    14-/
    15
    16namespace Lax606786.CocycleBasics
    17
    18open MeasureTheory TopologicalSpace
    19open Lax606786.Cocycles
    20
    21variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    22 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    23
    24/-- The iterates are strongly measurable. -/
    25axiom measurable_iterate_apply (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X]
    26 (n : ℕ) (x : X) : Measurable fun ω => R.iterate n ω x
    27
    28/-- `χ_k` is a.e. constant. -/
    29axiom exists_chi_ae_eq (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] (k : ℕ) :
    30 ∃ c : EReal, ∀ᵐ ω ∂(R.μ), R.chi k ω = c
    31
    32/-- The distinct exponent `λ_i` is a.e. constant. -/
    33axiom exists_lambda_ae_eq (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] (i : ℕ) :
    34 ∃ c : EReal, ∀ᵐ ω ∂(R.μ), R.lambda i ω = c
    35
    36/-- The multiplicity `m_i` is a.e. constant. -/
    37axiom exists_mult_ae_eq (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] (i : ℕ) :
    38 ∃ m : ℕ, ∀ᵐ ω ∂(R.μ), R.mult i ω = m
    39
    40end Lax606786.CocycleBasics
    41
    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…