Lax Lean Archive

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

Volume growth is comparable to products of Bernstein numbers

Lax606786.VolumeGrowthComparison · concepts/Lax606786/VolumeGrowthComparison.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 XX be a real normed space and k≥0k \ge 0. There are constants 0<c≤C0 < c \le C, depending only on kk, such that for every bounded operator TT on XX

    c Dk(T)≤ρ1(T)⋯ρk(T)≤C Dk(T).c\, D_k(T) \le \rho_1(T) \cdots \rho_k(T) \le C\, D_k(T).

    Moreover Dk(ST)≤Dk(S) Dk(T)D_k(ST) \le D_k(S)\, D_k(T), and there is K>0K > 0 depending only on kk with

    ∏i≤kρi(ST)≤K∏i≤kρi(S)∏i≤kρi(T).\prod_{i \le k} \rho_i(ST) \le K \prod_{i \le k} \rho_i(S) \prod_{i \le k} \rho_i(T).

    This is Lemma 8 of Lee (2024); the comparison follows the volume-growth arguments of González-Tokman and Quas (2015). Volume growth is also the basis of Blumenthal's (2016) approach to the multiplicative ergodic theorem.

    Concept map
    3 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.

    1 prod_bernsteinNumber_submultiplicative proven

    2 volumeGrowth_comparable proven

    3 volumeGrowth_submultiplicative proven

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.OperatorStatistics
    2
    3/-!
    4---
    5title: Volume growth is comparable to products of Bernstein numbers
    6type: theorem
    7---
    8Let XX be a real normed space and k≥0k \ge 0. There are constants 0<c≤C0 < c \le C, depending only
    9on kk, such that for every bounded operator TT on XX
    10c Dk(T)≤ρ1(T)⋯ρk(T)≤C Dk(T).c\, D_k(T) \le \rho_1(T) \cdots \rho_k(T) \le C\, D_k(T).
    11Moreover Dk(ST)≤Dk(S) Dk(T)D_k(ST) \le D_k(S)\, D_k(T), and there is K>0K > 0 depending only on kk with
    12∏i≤kρi(ST)≤K∏i≤kρi(S)∏i≤kρi(T).\prod_{i \le k} \rho_i(ST) \le K \prod_{i \le k} \rho_i(S) \prod_{i \le k} \rho_i(T).
    13This is Lemma 8 of Lee (2024); the comparison follows the volume-growth arguments of
    14González-Tokman and Quas (2015). Volume growth is also the basis of Blumenthal's (2016) approach to
    15the multiplicative ergodic theorem.
    16-/
    17
    18namespace Lax606786.VolumeGrowthComparison
    19
    20open Lax606786.OperatorStatistics
    21
    22variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    23
    24/-- `D_k` is comparable to `ρ_1 ⋯ ρ_k`, uniformly in the operator. -/
    25axiom volumeGrowth_comparable (k : ℕ) :
    26 ∃ c C : ℝ, 0 < c ∧ c ≤ C ∧ ∀ T : X →L[ℝ] X,
    27 c * volumeGrowth T k ≤ ∏ i ∈ Finset.range k, bernsteinNumber T (i + 1) ∧
    28 ∏ i ∈ Finset.range k, bernsteinNumber T (i + 1) ≤ C * volumeGrowth T k
    29
    30/-- `D_k` is submultiplicative. -/
    31axiom volumeGrowth_submultiplicative (k : ℕ) (T S : X →L[ℝ] X) :
    32 volumeGrowth (S.comp T) k ≤ volumeGrowth S k * volumeGrowth T k
    33
    34/-- `ρ_1 ⋯ ρ_k` is submultiplicative up to a constant. -/
    35axiom prod_bernsteinNumber_submultiplicative (k : ℕ) :
    36 ∃ K : ℝ, 0 < K ∧ ∀ S T : X →L[ℝ] X,
    37 ∏ i ∈ Finset.range k, bernsteinNumber (S.comp T) (i + 1)
    38 ≤ K * ((∏ i ∈ Finset.range k, bernsteinNumber S (i + 1)) *
    39 (∏ i ∈ Finset.range k, bernsteinNumber T (i + 1)))
    40
    41end Lax606786.VolumeGrowthComparison
    42
    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…