While this submission is a draft, it cannot be used by other submissions.

The signature of a modified cocycle

Lax606786.ModifiedCocycles · concepts/Lax606786/ModifiedCocycles.lean · lax-606786

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let L\mathcal{L} be a cocycle on a separable Banach space XX with its Borel σ\sigma-algebra. Let QωQ_\omega be strongly measurable, tempered, equivariant idempotents (QσωLω=LωQωQ_{\sigma\omega}\mathcal{L}_\omega = \mathcal{L}_\omega Q_\omega) with range a closed subspace V(ω)V(\omega) of codimension MM and kernel F(ω)F(\omega), and suppose F(ω)F(\omega) grows strictly faster than Lω(n)Qω\mathcal{L}^{(n)}_\omega Q_\omega for large nn. Let AA be a measurable set of positive measure on which ∥Qω∥\|Q_\omega\| is bounded.

    If L′\mathcal{L}' is the cocycle over the same base with generator LωQω\mathcal{L}_\omega Q_\omega on AA and Lω\mathcal{L}_\omega off AA, then almost surely its signature is that of L\mathcal{L} shifted by MM: χk′=χM+k\chi'_k = \chi_{M+k} for all k≥1k \ge 1.

    Concept map
    6 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Lean source view on GitLab

    1import Lax606786.Cocycles
    2import Lax606786.BanachGrassmannian
    3
    4/-!
    5---
    6title: The signature of a modified cocycle
    7type: theorem
    8---
    9Let L\mathcal{L} be a cocycle on a separable Banach space XX with its Borel σ\sigma-algebra.
    10Let QωQ_\omega be strongly measurable, tempered, equivariant idempotents
    11(QσωLω=LωQωQ_{\sigma\omega}\mathcal{L}_\omega = \mathcal{L}_\omega Q_\omega) with range a closed subspace
    12V(ω)V(\omega) of codimension MM and kernel F(ω)F(\omega), and suppose F(ω)F(\omega) grows strictly faster
    13than Lω(n)Qω\mathcal{L}^{(n)}_\omega Q_\omega for large nn. Let AA be a measurable set of positive
    14measure on which ∥Qω∥\|Q_\omega\| is bounded.
    15
    16If L′\mathcal{L}' is the cocycle over the same base with generator LωQω\mathcal{L}_\omega Q_\omega on
    17AA and Lω\mathcal{L}_\omega off AA, then almost surely its signature is that of L\mathcal{L}
    18shifted by MM: χk′=χM+k\chi'_k = \chi_{M+k} for all k≥1k \ge 1.
    19-/
    20
    21namespace Lax606786.ModifiedCocycles
    22
    23open MeasureTheory Filter TopologicalSpace
    24open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.OperatorStatistics
    25
    26open Classical in
    27/-- The modified cocycle has the signature of `R` shifted by the codimension of `V`. -/
    28axiom 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
    45end Lax606786.ModifiedCocycles
    46
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…