The signature of a modified cocycle
Lax606786.ModifiedCocycles · concepts/Lax606786/ModifiedCocycles.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 with its Borel -algebra. Let be strongly measurable, tempered, equivariant idempotents () with range a closed subspace of codimension and kernel , and suppose grows strictly faster than for large . Let be a measurable set of positive measure on which is bounded.
If is the cocycle over the same base with generator on and off , then almost surely its signature is that of shifted by : for all .
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitLab
| 1 | import Lax606786.Cocycles |
| 2 | import Lax606786.BanachGrassmannian |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: The signature of a modified cocycle |
| 7 | type: theorem |
| 8 | --- |
| 9 | Let be a cocycle on a separable Banach space with its Borel -algebra. |
| 10 | Let be strongly measurable, tempered, equivariant idempotents |
| 11 | () with range a closed subspace |
| 12 | of codimension and kernel , and suppose grows strictly faster |
| 13 | than for large . Let be a measurable set of positive |
| 14 | measure on which is bounded. |
| 15 | |
| 16 | If is the cocycle over the same base with generator on |
| 17 | and off , then almost surely its signature is that of |
| 18 | shifted by : for all . |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax606786.ModifiedCocycles |
| 22 | |
| 23 | open MeasureTheory Filter TopologicalSpace |
| 24 | open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.OperatorStatistics |
| 25 | |
| 26 | open Classical in |
| 27 | /-- The modified cocycle has the signature of `R` shifted by the codimension of `V`. -/ |
| 28 | axiom chi_modify {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] |
| 29 | [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X] |
| 30 | (R R' : Cocycle Ω X) [SeparableSpace X] [BorelSpace X] {M : ℕ} |
| 31 | (F : Ω → Submodule ℝ X) (V : Ω → GrassmannianCofin X M) (Q : Ω → X →L[ℝ] X) |
| 32 | (hQm : ∀ x, Measurable fun ω => Q ω x) {A : Set Ω} (hA : MeasurableSet A) |
| 33 | (hApos : R.μ A ≠ 0) {C : ℝ} (hC : ∀ ω ∈ A, ‖Q ω‖ ≤ C) |
| 34 | (hσ : R'.σ = R.σ) (hμ : R'.μ = R.μ) |
| 35 | (hL : ∀ ω, R'.L ω = if ω ∈ A then (R.L ω).comp (Q ω) else R.L ω) |
| 36 | (hidem : ∀ᵐ ω ∂(R.μ), (Q ω).comp (Q ω) = Q ω) |
| 37 | (hrange : ∀ᵐ ω ∂(R.μ), LinearMap.range (Q ω : X →ₗ[ℝ] X) = ((V ω).1.1 : Submodule ℝ X)) |
| 38 | (hker : ∀ᵐ ω ∂(R.μ), LinearMap.ker (Q ω : X →ₗ[ℝ] X) = F ω) |
| 39 | (heq : ∀ᵐ ω ∂(R.μ), (Q (R.σ ω)).comp (R.L ω) = (R.L ω).comp (Q ω)) |
| 40 | (htemp : R.IsTempered Q) |
| 41 | (hgap : ∀ᵐ ω ∂(R.μ), ∀ᶠ n : ℕ in atTop, |
| 42 | ‖(R.iterate n ω).comp (Q ω)‖ < growth (R.iterate n ω) (F ω)) : |
| 43 | ∀ᵐ ω ∂(R.μ), ∀ k : ℕ, 1 ≤ k → R'.chi k ω = R.chi (M + k) ω |
| 44 | |
| 45 | end Lax606786.ModifiedCocycles |
| 46 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments