Lax Lean Archive

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

Gelfand numbers, Bernstein numbers and the compactness seminorm

Lax606786.GelfandBernsteinComparison · concepts/Lax606786/GelfandBernsteinComparison.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, TT a bounded operator on XX and k≥1k \ge 1. Then

    ρk(T)≤sk(T)≤4k−1(k−1)! ρk(T)and∥T∥c≤2k sk(T).\rho_k(T) \le s_k(T) \le 4^{k-1}(k-1)!\,\rho_k(T) \qquad \text{and} \qquad \|T\|_c \le 2k\, s_k(T).

    The first inequality holds for every kk. These are Lemmas 31–33 of Lee (2024). Sharper constants follow from the Kadec–Snobar theorem (Kadec and Snobar 1971; see also Wojtaszczyk 1991, III.B.10) and from Pietsch's theory of ss-numbers (Pietsch 1974); any constant depending on kk alone suffices for comparing exponential growth rates.

    Gelfand numbers are nonnegative.

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

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

    1 bernsteinNumber_le_gelfandNumber proven

    2 compactSeminorm_le_gelfandNumber proven

    3 gelfandNumber_le_bernsteinNumber proven

    4 gelfandNumber_nonneg proven

    In the paper

    • page 17 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.OperatorStatistics
    2
    3/-!
    4---
    5title: Gelfand numbers, Bernstein numbers and the compactness seminorm
    6type: theorem
    7---
    8Let XX be a real normed space, TT a bounded operator on XX and k≥1k \ge 1. Then
    9ρk(T)≤sk(T)≤4k−1(k−1)! ρk(T)and∥T∥c≤2k sk(T).\rho_k(T) \le s_k(T) \le 4^{k-1}(k-1)!\,\rho_k(T) \qquad \text{and} \qquad \|T\|_c \le 2k\, s_k(T).
    10
    11The first inequality holds for every kk. These are Lemmas 31–33 of Lee (2024). Sharper constants
    12follow from the Kadec–Snobar theorem (Kadec and Snobar 1971; see also Wojtaszczyk 1991, III.B.10) and from
    13Pietsch's theory of ss-numbers (Pietsch 1974); any constant depending on kk alone suffices for
    14comparing exponential growth rates.
    15
    16Gelfand numbers are nonnegative.
    17-/
    18
    19namespace Lax606786.GelfandBernsteinComparison
    20
    21open Lax606786.OperatorStatistics
    22
    23variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    24
    25/-- `ρ_k ≤ s_k`. -/
    26axiom bernsteinNumber_le_gelfandNumber (T : X →L[ℝ] X) (k : ℕ) :
    27 bernsteinNumber T k ≤ gelfandNumber T k
    28
    29/-- `s_k ≤ 4^{k-1} (k-1)! ρ_k`. -/
    30axiom gelfandNumber_le_bernsteinNumber (T : X →L[ℝ] X) {k : ℕ} (hk : 1 ≤ k) :
    31 gelfandNumber T k ≤ 4 ^ (k - 1) * (Nat.factorial (k - 1) : ℝ) * bernsteinNumber T k
    32
    33/-- `‖T‖_c ≤ 2k s_k`. -/
    34axiom compactSeminorm_le_gelfandNumber (T : X →L[ℝ] X) {k : ℕ} (hk : 1 ≤ k) :
    35 compactSeminorm T ≤ 2 * (k : ℝ) * gelfandNumber T k
    36
    37/-- Gelfand numbers are nonnegative. -/
    38axiom gelfandNumber_nonneg (T : X →L[ℝ] X) (k : ℕ) : 0 ≤ gelfandNumber T k
    39
    40end Lax606786.GelfandBernsteinComparison
    41
    Show ProofShow 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…