Lax Lean Archive

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

Constructing the Oseledets decomposition with subspace growth estimates

lax-606786·formalized by George Lee·created ·GitLab @7325fb4·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    A formalisation of the semi-invertible multiplicative ergodic theorem for strongly measurable, forward-integrable cocycles L\mathcal L of bounded operators on a separable Banach space XX, over an invertible ergodic transformation of a Lebesgue probability space. No invertibility or injectivity of the operators Lω\mathcal L_\omega is assumed.

    The Lyapunov exponents are defined through the growth rates χk\chi_k of the Bernstein numbers of the iterates Lω(n)\mathcal L^{(n)}_\omega, and the distinct exponents λ1>λ2>⋯\lambda_1 > \lambda_2 > \cdots are read off from them. The main result is the Oseledets decomposition: for each ll the space splits almost surely as X=E1(ω)⊕⋯⊕El−1(ω)⊕Vl(ω)X = E_1(\omega) \oplus \cdots \oplus E_{l-1}(\omega) \oplus V_l(\omega) into equivariant, measurable, finite-dimensional fast spaces Ei(ω)E_i(\omega), on which the cocycle grows at rate exactly λi\lambda_i both in norm and in slowest growth, and an invariant slow space Vl(ω)={x:λω(x)≤λl}V_l(\omega) = \{x : \lambda_\omega(x) \le \lambda_l\}, with strongly measurable, tempered projections. The decomposition is nontrivial exactly when the cocycle is quasicompact.

    The submission also proves that the decomposition is unique, that the sum of the first ii fast spaces is exactly the set of vectors admitting a backward history decaying at rate λi\lambda_i, and that the index of compactness lim⁡kχk\lim_k \chi_k agrees with the growth rate of the distance of Lω(n)\mathcal L^{(n)}_\omega to the compact operators, so that quasicompactness can be read off from that growth rate. The proofs include a version of Kingman's subadditive ergodic theorem for balanced time intervals, and Birkhoff's ergodic theorem.

    View annotated paper

    18 pages · 10 marked passages

    Concepts

    Concept map
    18 concepts
    100%
    Proven claimDefinitionThis submissionA → B: B builds on A

    Proofs

    Proof networkview on GitLab

    100%
    assumptions conclusionProven claimClaim from this submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitLab

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    No other submission in the archive builds on this one, and this one builds on none.

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-606786,
  author = {George Lee},
  title = {Constructing the Oseledets decomposition with subspace growth estimates},
  year = {2026},
  howpublished = {Lax Archive, lax-606786},
  url = {https://laxarchive.org/lax-606786/},
  note = {draft},
}

    References

    1. George Lee. Constructing the Oseledets decomposition with subspace growth estimates. Transactions of the American Mathematical Society, Series B 11:396–419, 2024. doi:10.1090/btran/146
    2. Joseph Anthony Horan. Spectral gap and asymptotics for a family of cocycles of Perron–Frobenius operators. University of Victoria, 2020. dspace.library.uvic.ca/items/f06cd01d-72c0-446f-afc4-bed2be0dcf77
    3. V. I. Oseledets. A multiplicative ergodic theorem. Characteristic Ljapunov, exponents of dynamical systems. Trudy Moskovskogo Matematicheskogo Obshchestva 19:179–210, 1968.
    4. G. Froyland, S. Lloyd and A. Quas. A semi-invertible Oseledets Theorem with applications to transfer operator cocycles. Discrete and Continuous Dynamical Systems 33:3835–3860, 2013. doi:10.3934/dcds.2013.33.3835
    5. C. González-Tokman and A. Quas. A semi-invertible operator Oseledets theorem. Ergodic Theory and Dynamical Systems 34(4):1230–1272, 2014. doi:10.1017/etds.2012.189
    6. C. González-Tokman and A. Quas. A concise proof of the multiplicative ergodic theorem on Banach spaces. Journal of Modern Dynamics 9(01):237–255, 2015.
    7. R. Mañé. Lyapounov exponents and stable manifolds for compact transformations. In Geometric dynamics 522–577, 1983.
    8. G. D. Birkhoff. Proof of the ergodic theorem. Proceedings of the National Academy of Sciences 17(12):656–660, 1931. doi:10.1073/pnas.17.12.656
    9. J. von Neumann. Proof of the quasi-ergodic hypothesis. Proceedings of the National Academy of Sciences 18(1):70–82, 1932. doi:10.1073/pnas.18.1.70
    10. A. M. Garsia. A simple proof of E. Hopf's maximal ergodic theorem. Journal of Mathematics and Mechanics 14:381–382, 1965.
    11. J. F. C. Kingman. The ergodic theory of subadditive stochastic processes. Journal of the Royal Statistical Society: Series B (Methodological) 30(3):499–510, 1968.
    12. J. M. Steele. Kingman's subadditive ergodic theorem. Annales de l'Institut Henri Poincaré, Probabilités et Statistiques 25(1):93–98, 1989.
    13. D. J. Rudolph. Fundamentals of Measurable Dynamics: Ergodic Theory on Lebesgue Spaces. Clarendon Press, 1990.
    14. A. Pietsch. s-Numbers of operators in Banach spaces. Studia Mathematica 51(3):201-223, 1974. eudml.org/doc/217913

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…