Vectors with decaying backward histories form subspaces
Lax606786.BackwardHistoryProperties · concepts/Lax606786/BackwardHistoryProperties.lean · lax-606786
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let be a cocycle on a Banach space , and the set of vectors with a backward history at decaying at rate . Then
- each is a linear subspace of , and for ;
- if is separable with its Borel -algebra and is a measurable family with almost surely, growing at rate at least (for every , for all large , almost surely), then almost surely.
Concept map
Evidence
Lean source view on GitLab
| 1 | import Lax606786.BackwardHistories |
| 2 | import Lax606786.BanachGrassmannian |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Vectors with decaying backward histories form subspaces |
| 7 | type: theorem |
| 8 | --- |
| 9 | Let be a cocycle on a Banach space , and the set of vectors with a |
| 10 | backward history at decaying at rate . Then |
| 11 | |
| 12 | - each is a linear subspace of , and for |
| 13 | ; |
| 14 | - if is separable with its Borel -algebra and is a |
| 15 | measurable family with almost surely, growing at |
| 16 | rate at least (for every , for all |
| 17 | large , almost surely), then almost surely. |
| 18 | -/ |
| 19 | |
| 20 | namespace Lax606786.BackwardHistoryProperties |
| 21 | |
| 22 | open MeasureTheory Filter TopologicalSpace |
| 23 | open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.OperatorStatistics |
| 24 | Lax606786.BackwardHistories |
| 25 | |
| 26 | variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] |
| 27 | [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X] |
| 28 | |
| 29 | /-- `B_c(ω)` is the carrier of a subspace of `X`. -/ |
| 30 | axiom exists_submodule_eq_backwardSet (R : Cocycle Ω X) (ω : Ω) (c : EReal) : |
| 31 | ∃ B : Submodule ℝ X, (B : Set X) = backwardSet R ω c |
| 32 | |
| 33 | /-- `B_c(ω) ⊆ B_{c'}(ω)` for `c' ≤ c`. -/ |
| 34 | axiom backwardSet_anti (R : Cocycle Ω X) (ω : Ω) {c c' : EReal} (h : c' ≤ c) : |
| 35 | backwardSet R ω c ⊆ backwardSet R ω c' |
| 36 | |
| 37 | /-- An equivariant measurable family growing at rate at least `c` lies in `B_c`. -/ |
| 38 | axiom ae_subset_backwardSet_of_growth (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] |
| 39 | {m : ℕ} [NeZero m] (E : Ω → GrassmannianFin X m) (hEm : Measurable E) |
| 40 | (hEeq : ∀ᵐ ω ∂(R.μ), Submodule.map (R.L ω : X →ₗ[ℝ] X) ((E ω).1 : Submodule ℝ X) |
| 41 | = ((E (R.σ ω)).1 : Submodule ℝ X)) |
| 42 | {c : ℝ} (hEg : ∀ᵐ ω ∂(R.μ), ∀ b : ℝ, b < c → ∀ᶠ n : ℕ in atTop, |
| 43 | Real.exp (b * n) ≤ growth (R.iterate n ω) ((E ω).1 : Submodule ℝ X)) : |
| 44 | ∀ᵐ ω ∂(R.μ), ((E ω).1 : Set X) ⊆ backwardSet R ω c |
| 45 | |
| 46 | end Lax606786.BackwardHistoryProperties |
| 47 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments