Lax Lean Archive

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

The index of compactness is the growth rate of the compactness seminorm

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

proven

Loading review…

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. If the growth rate of the compactness seminorm of the iterates exists and is almost everywhere equal to a constant κ∈[−∞,∞]\kappa \in [-\infty, \infty],

    lim⁡n1nlog⁡∥Lω(n)∥c=κfor a.e. ω,\lim_n \tfrac1n \log \|\mathcal{L}^{(n)}_\omega\|_c = \kappa \quad \text{for a.e. } \omega,

    then the index of compactness ν=lim⁡kχk\nu = \lim_k \chi_k equals κ\kappa almost everywhere. This is the equivalence of growth statistics in the appendix of Lee (2024).

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 17 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.Cocycles
    2
    3/-!
    4---
    5title: The index of compactness is the growth rate of the compactness seminorm
    6type: theorem
    7---
    8Let L\mathcal{L} be a cocycle on a separable Banach space XX. If the growth rate of the
    9compactness seminorm of the iterates exists and is almost everywhere equal to a constant
    10κ∈[−∞,∞]\kappa \in [-\infty, \infty],
    11lim⁡n1nlog⁡∥Lω(n)∥c=κfor a.e. ω,\lim_n \tfrac1n \log \|\mathcal{L}^{(n)}_\omega\|_c = \kappa \quad \text{for a.e. } \omega,
    12then the index of compactness ν=lim⁡kχk\nu = \lim_k \chi_k equals κ\kappa almost everywhere. This is
    13the equivalence of growth statistics in the appendix of Lee (2024).
    14-/
    15
    16namespace Lax606786.IndexOfCompactness
    17
    18open MeasureTheory Filter TopologicalSpace
    19open Lax606786.OperatorStatistics Lax606786.ExtendedLog Lax606786.Cocycles
    20
    21/-- `ν = κ` almost everywhere, where `κ` is the growth rate of `‖𝓛^{(n)}_ω‖_c`. -/
    22axiom nu_eq_compactnessIndex {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
    23 [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
    24 (R : Cocycle Ω X) [SeparableSpace X] [BorelSpace X]
    25 (κ : EReal) (hκ : ∀ᵐ ω ∂(R.μ), Tendsto (fun n : ℕ =>
    26 logEReal (compactSeminorm (R.iterate n ω)) / (n : EReal)) atTop (nhds κ)) :
    27 ∀ᵐ ω ∂(R.μ), R.nu ω = κ
    28
    29end Lax606786.IndexOfCompactness
    30
    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…