Quasicompactness in terms of the compactness seminorm
Lax606786.QuasicompactnessCriterion · concepts/Lax606786/QuasicompactnessCriterion.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 that
for a constant . Then is quasicompact if and only if almost everywhere. Combined with the Oseledets decomposition, the decomposition is nontrivial () exactly when the growth rate of is strictly smaller than that of .
Concept map
Lean source view on GitLab
| 1 | import Lax606786.Cocycles |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Quasicompactness in terms of the compactness seminorm |
| 6 | type: theorem |
| 7 | --- |
| 8 | Let be a cocycle on a separable Banach space , and suppose that |
| 9 | |
| 10 | for a constant . Then is quasicompact if and only if |
| 11 | almost everywhere. Combined with the Oseledets decomposition, the |
| 12 | decomposition is nontrivial () exactly when the growth rate of |
| 13 | is strictly smaller than that of . |
| 14 | -/ |
| 15 | |
| 16 | namespace Lax606786.QuasicompactnessCriterion |
| 17 | |
| 18 | open MeasureTheory Filter TopologicalSpace |
| 19 | open Lax606786.OperatorStatistics Lax606786.ExtendedLog Lax606786.Cocycles |
| 20 | |
| 21 | /-- Quasicompactness is `κ < λ₁`, for the growth rate `κ` of `‖𝓛^{(n)}_ω‖_c`. -/ |
| 22 | axiom isQuasicompact_iff {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] |
| 23 | [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X] |
| 24 | (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] |
| 25 | (κ : EReal) (hκ : ∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ => |
| 26 | logEReal (compactSeminorm (R.iterate n ω)) / (n : EReal)) atTop (nhds κ)) : |
| 27 | R.IsQuasicompact ↔ ∀ᵐ ω ∂(R.μ), κ < R.chi 1 ω |
| 28 | |
| 29 | end Lax606786.QuasicompactnessCriterion |
| 30 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments