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

Vectors with decaying backward histories form subspaces

Lax606786.BackwardHistoryProperties · concepts/Lax606786/BackwardHistoryProperties.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 Banach space XX, and Bc(ω)B_c(\omega) the set of vectors with a backward history at ω\omega decaying at rate cc. Then

    • each Bc(ω)B_c(\omega) is a linear subspace of XX, and Bc(ω)⊆Bc′(ω)B_c(\omega) \subseteq B_{c'}(\omega) for c′≤cc' \le c;
    • if XX is separable with its Borel σ\sigma-algebra and E:Ω→GmXE : \Omega \to \mathcal{G}_m X is a measurable family with LωE(ω)=E(σω)\mathcal{L}_\omega E(\omega) = E(\sigma\omega) almost surely, growing at rate at least cc (for every b<cb < c, g(Lω(n),E(ω))≥ebng(\mathcal{L}^{(n)}_\omega, E(\omega)) \ge e^{bn} for all large nn, almost surely), then E(ω)⊆Bc(ω)E(\omega) \subseteq B_c(\omega) almost surely.
    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    Lean source view on GitLab

    1import Lax606786.BackwardHistories
    2import Lax606786.BanachGrassmannian
    3
    4/-!
    5---
    6title: Vectors with decaying backward histories form subspaces
    7type: theorem
    8---
    9Let L\mathcal{L} be a cocycle on a Banach space XX, and Bc(ω)B_c(\omega) the set of vectors with a
    10backward history at ω\omega decaying at rate cc. Then
    11
    12- each Bc(ω)B_c(\omega) is a linear subspace of XX, and Bc(ω)⊆Bc′(ω)B_c(\omega) \subseteq B_{c'}(\omega) for
    13 c′≤cc' \le c;
    14- if XX is separable with its Borel σ\sigma-algebra and E:Ω→GmXE : \Omega \to \mathcal{G}_m X is a
    15 measurable family with LωE(ω)=E(σω)\mathcal{L}_\omega E(\omega) = E(\sigma\omega) almost surely, growing at
    16 rate at least cc (for every b<cb < c, g(Lω(n),E(ω))≥ebng(\mathcal{L}^{(n)}_\omega, E(\omega)) \ge e^{bn} for all
    17 large nn, almost surely), then E(ω)⊆Bc(ω)E(\omega) \subseteq B_c(\omega) almost surely.
    18-/
    19
    20namespace Lax606786.BackwardHistoryProperties
    21
    22open MeasureTheory Filter TopologicalSpace
    23open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.OperatorStatistics
    24 Lax606786.BackwardHistories
    25
    26variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    27 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    28
    29/-- `B_c(ω)` is the carrier of a subspace of `X`. -/
    30axiom 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`. -/
    34axiom 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`. -/
    38axiom 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
    46end Lax606786.BackwardHistoryProperties
    47
    Show ProofShow ProofShow 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…