Fast spaces
Lax606786.FastSpaces · concepts/Lax606786/FastSpaces.lean · lax-606786
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
Let be a cocycle on and . A family of -dimensional subspaces is a fast space of multiplicity at rate when it is measurable and equivariant ( almost surely), and almost surely every nonzero vector of has growth rate and .
Concept map
Lean source view on GitLab
| 1 | import Lax606786.Cocycles |
| 2 | import Lax606786.BanachGrassmannian |
| 3 | import Lax606786.ExtendedLog |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: Fast spaces |
| 8 | type: definition |
| 9 | --- |
| 10 | Let be a cocycle on and . A family |
| 11 | of -dimensional subspaces is a *fast space* of |
| 12 | multiplicity at rate when it is measurable and equivariant |
| 13 | ( almost surely), and almost surely every nonzero |
| 14 | vector of has growth rate and |
| 15 | . |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax606786.FastSpaces |
| 19 | |
| 20 | open MeasureTheory Filter |
| 21 | open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.OperatorStatistics |
| 22 | Lax606786.ExtendedLog |
| 23 | |
| 24 | /-- `E` is a fast space of multiplicity `k` at rate `lam`. -/ |
| 25 | def IsFastSpace {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] |
| 26 | [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X] |
| 27 | (R : Cocycle Ω X) (k : ℕ) [NeZero k] (lam : ℝ) (E : Ω → GrassmannianFin X k) : Prop := |
| 28 | Measurable E ∧ |
| 29 | (∀ᵐ ω ∂(R.μ), ∀ x ∈ (E ω).1, x ≠ 0 → R.lambdaAt ω x = (lam : EReal)) ∧ |
| 30 | (∀ᵐ ω ∂(R.μ), (E ω).1.map (R.L ω : X →ₗ[ℝ] X) = (E (R.σ ω)).1) ∧ |
| 31 | (∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ => logEReal (growth (R.iterate n ω) (E ω).1) / (n : EReal)) |
| 32 | atTop (nhds (lam : EReal))) |
| 33 | |
| 34 | end Lax606786.FastSpaces |
| 35 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments