Lax Lean Archive

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

Constructing the levels of the decomposition

Lax606786.LevelConstruction · concepts/Lax606786/LevelConstruction.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, and let λi\lambda_i be almost surely its distinct exponents.

    • (Base.) If L\mathcal{L} is quasicompact, there is a decomposition after the first fast space, with F=E=E1F = E = E_1.
    • (Step.) If DD is a decomposition after the first ll fast spaces and ml+1≠0m_{l+1} \ne 0 almost surely, there is a decomposition D′D' after the first l+1l + 1, with F′=F⊕E′F' = F \oplus E'.

    These are the base case and inductive step of the proof of Theorem 3 of Lee (2024).

    Concept map
    7 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 exists_level_one proven

    2 exists_level_succ proven

    Lean source view on GitLab

    1import Lax606786.OseledetsLevels
    2
    3/-!
    4---
    5title: Constructing the levels of the decomposition
    6type: theorem
    7---
    8Let L\mathcal{L} be a cocycle on a separable Banach space XX with its Borel σ\sigma-algebra, and
    9let λi\lambda_i be almost surely its distinct exponents.
    10
    11- (Base.) If L\mathcal{L} is quasicompact, there is a decomposition after the first fast space,
    12 with F=E=E1F = E = E_1.
    13- (Step.) If DD is a decomposition after the first ll fast spaces and ml+1≠0m_{l+1} \ne 0
    14 almost surely, there is a decomposition D′D' after the first l+1l + 1, with
    15 F′=F⊕E′F' = F \oplus E'.
    16
    17These are the base case and inductive step of the proof of Theorem 3 of Lee (2024).
    18-/
    19
    20namespace Lax606786.LevelConstruction
    21
    22open MeasureTheory TopologicalSpace
    23open Lax606786.Cocycles Lax606786.OseledetsLevels
    24
    25/-- The base level: the top fast space and its slow complement. -/
    26axiom exists_level_one {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    27 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    28 (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X]
    29 [CompleteSpace X] {lam : ℕ → EReal} (hlam : ∀ i, ∀ᵐ ω ∂(R.μ), R.lambda i ω = lam i)
    30 (hqc : R.IsQuasicompact) :
    31 ∃ D : LevelData Ω X, IsLevel R lam 1 D ∧
    32 ∀ᵐ ω ∂(R.μ), ((D.F ω).1 : Submodule ℝ X) = ((D.E ω).1 : Submodule ℝ X)
    33
    34/-- The inductive step: the next fast space, split off the current slow space. -/
    35axiom exists_level_succ {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    36 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    37 (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X]
    38 [CompleteSpace X] {lam : ℕ → EReal} (hlam : ∀ i, ∀ᵐ ω ∂(R.μ), R.lambda i ω = lam i)
    39 {l : ℕ} {D : LevelData Ω X} (hD : IsLevel R lam l D)
    40 (hm : ∀ᵐ ω ∂(R.μ), R.mult (l + 1) ω ≠ 0) :
    41 ∃ D' : LevelData Ω X, IsLevel R lam (l + 1) D' ∧
    42 ∀ᵐ ω ∂(R.μ), ((D'.F ω).1 : Submodule ℝ X) = ((D.F ω).1 : Submodule ℝ X) ⊔
    43 ((D'.E ω).1 : Submodule ℝ X)
    44
    45end Lax606786.LevelConstruction
    46
    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…