The Oseledets filtration theorem, dimension-zero case #
This module proves Oseledets.oseledets_filtration_dim_zero, the trivial d = 0 base case of
the Oseledets multiplicative ergodic theorem Oseledets.oseledets_filtration (see
Oseledets/MultiplicativeErgodic.lean). When the ambient space is EuclideanSpace ℝ (Fin 0)
there are no exponents (k = 0) and the single subspace ⊤ = ⊥ is the whole (zero) space, so
every conjunct of the conclusion holds trivially. The main theorem composes this with the
positive-dimensional Oseledets.oseledets_filtration_of_topgap.
Main results #
Oseledets.oseledets_filtration_dim_zero: the dimension-zero case of the Oseledets filtration theorem.
theorem
Oseledets.oseledets_filtration_dim_zero
{X : Type u_1}
[MeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsProbabilityMeasure μ]
{T : X → X}
(_hT : Ergodic T μ)
(A : X → Matrix (Fin 0) (Fin 0) ℝ)
(_hA : ∀ (x : X), (A x).det ≠ 0)
(_hAmeas : Measurable A)
(_hint : IntegrableLogNorm A μ)
(_hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ)
:
∃ (k : ℕ) (lam : Fin k → ℝ) (V : Fin (k + 1) → X → Submodule ℝ (EuclideanSpace ℝ (Fin 0))),
StrictAnti lam ∧ (∀ (i : Fin (k + 1)), MeasurableSubspace fun (x : X) => V i x) ∧ ∀ᵐ (x : X) ∂μ, V 0 x = ⊤ ∧ V (Fin.last k) x = ⊥ ∧ (∀ (i : Fin k), V i.succ x < V i.castSucc x) ∧ (∀ (i : Fin (k + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (A x))) (V i x) = V i (T x)) ∧ ∀ (i : Fin k),
∀ v ∈ ↑(V i.castSucc x),
v ∉ V i.succ x →
Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A T n x)) v‖)
Filter.atTop (nhds (lam i))
The Oseledets filtration theorem, dimension-zero case.
Trivial: k = 0, V ≡ ⊤ = ⊥.