The Oseledets decomposition is nontrivial exactly when the compactness growth rate is smaller
Lax606786.OseledetsCompactnessCriterion · concepts/Lax606786/OseledetsCompactnessCriterion.lean · lax-606786
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let be a cocycle on a separable Banach space , and suppose the growth rate of the compactness seminorm of its iterates is almost everywhere a constant :
Then for any Oseledets decomposition of , the top exponent satisfies , and the decomposition is nontrivial () exactly when . This is the last clause of Theorem 3 of Lee (2024), with the index of compactness in place of . Such a always exists, by the concept ().
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitLab
| 1 | import Lax606786.OseledetsDecompositions |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The Oseledets decomposition is nontrivial exactly when the compactness growth rate is smaller |
| 6 | type: theorem |
| 7 | --- |
| 8 | Let be a cocycle on a separable Banach space , and suppose the growth rate of the |
| 9 | compactness seminorm of its iterates is almost everywhere a constant : |
| 10 | |
| 11 | Then for any Oseledets decomposition of , the top exponent |
| 12 | satisfies , and |
| 13 | the decomposition is nontrivial () exactly when . This is the last |
| 14 | clause of Theorem 3 of Lee (2024), with the index of compactness in place of . |
| 15 | Such a always exists, by the concept `IndexOfCompactness` (`exists_compactnessIndex`). |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax606786.OseledetsCompactnessCriterion |
| 19 | |
| 20 | open MeasureTheory Filter TopologicalSpace |
| 21 | open Lax606786.BanachGrassmannian Lax606786.OperatorStatistics Lax606786.ExtendedLog |
| 22 | Lax606786.Cocycles Lax606786.OseledetsDecompositions |
| 23 | |
| 24 | /-- `κ ≤ λ₁`, and `L ≥ 2` exactly when `κ ≠ λ₁`. -/ |
| 25 | axiom kappa_le_and_two_le_iff {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] |
| 26 | [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X] |
| 27 | (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] |
| 28 | (κ : EReal) (hκ : ∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ => |
| 29 | logEReal (compactSeminorm (R.iterate n ω)) / (n : EReal)) atTop (nhds κ)) |
| 30 | {L : ℕ∞} {lam : ℕ → EReal} {m : ℕ → ℕ+} |
| 31 | {E : ∀ i : ℕ, 1 ≤ i → (i : ℕ∞) < L → Ω → GrassmannianFin X (m i)} |
| 32 | {V : ℕ → Ω → Submodule ℝ X} {P : ℕ → Ω → X →L[ℝ] X} |
| 33 | (h : IsOseledetsDecomposition R L lam m E V P) : |
| 34 | κ ≤ lam 1 ∧ ((2 : ℕ∞) ≤ L ↔ κ ≠ lam 1) |
| 35 | |
| 36 | end Lax606786.OseledetsCompactnessCriterion |
| 37 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments