This site hosts the blueprint and the API documentation of a Lean 4 + Mathlib formalization of the Oseledets multiplicative ergodic theorem (MET).
Three headline theorems are formalized, sorry-free:
Oseledets.oseledets_filtration— the one-sided MET (filtration form);Oseledets.oseledets_splitting— the two-sided splitting;Oseledets.oseledets_flow— the continuous-flow MET.
together with a layer of companion results (the Lyapunov spectrum, exponent sums, the trace–determinant identity, exterior/wedge growth, the inverse spectrum, restriction to invariant subbundles, the non-ergodic spectrum, regularity of the exponents, and singular one-sided bounds).
Useful links: