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

Elementary properties of Bernstein numbers

Lax606786.BernsteinNumberProperties · concepts/Lax606786/BernsteinNumberProperties.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 XX be a real normed space and S,TS, T bounded operators on XX.

    • ρ0(T)=0\rho_0(T) = 0, ρ1(T)=∥T∥\rho_1(T) = \|T\|, 0≤ρk(T)≤∥T∥0 \le \rho_k(T) \le \|T\|, and ρq(T)≤ρp(T)\rho_q(T) \le \rho_p(T) for 1≤p≤q1 \le p \le q.
    • g(T,V)≤ρm(T)g(T, V) \le \rho_m(T) for every V∈GmXV \in \mathcal{G}_m X, and ρ1(T)⋯ρk(T)≤∥T∥k\rho_1(T) \cdots \rho_k(T) \le \|T\|^k.

    For every kk,

    ρk(ST)≤ρk(S) ∥T∥andρk(ST)≤∥S∥ ρk(T).\rho_k(S T) \le \rho_k(S)\,\|T\| \qquad \text{and} \qquad \rho_k(S T) \le \|S\|\,\rho_k(T).

    Moreover, for k≥1k \ge 1 the growth g(T,V)g(T, V) is jointly continuous in (T,V)(T, V), for the operator norm on TT and the Hausdorff distance between unit spheres on V∈GkXV \in \mathcal{G}_k X.

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

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

    3 bernsteinNumber_comp_le_norm_mul proven

    5 bernsteinNumber_nonneg proven

    6 bernsteinNumber_one proven

    7 bernsteinNumber_zero proven

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.OperatorStatistics
    2
    3/-!
    4---
    5title: Elementary properties of Bernstein numbers
    6type: theorem
    7---
    8Let XX be a real normed space and S,TS, T bounded operators on XX.
    9
    10- ρ0(T)=0\rho_0(T) = 0, ρ1(T)=∥T∥\rho_1(T) = \|T\|, 0≤ρk(T)≤∥T∥0 \le \rho_k(T) \le \|T\|, and
    11 ρq(T)≤ρp(T)\rho_q(T) \le \rho_p(T) for 1≤p≤q1 \le p \le q.
    12- g(T,V)≤ρm(T)g(T, V) \le \rho_m(T) for every V∈GmXV \in \mathcal{G}_m X, and
    13 ρ1(T)⋯ρk(T)≤∥T∥k\rho_1(T) \cdots \rho_k(T) \le \|T\|^k.
    14
    15For every kk,
    16ρk(ST)≤ρk(S) ∥T∥andρk(ST)≤∥S∥ ρk(T).\rho_k(S T) \le \rho_k(S)\,\|T\| \qquad \text{and} \qquad \rho_k(S T) \le \|S\|\,\rho_k(T).
    17Moreover, for k≥1k \ge 1 the growth g(T,V)g(T, V) is jointly continuous in (T,V)(T, V), for the operator
    18norm on TT and the Hausdorff distance between unit spheres on V∈GkXV \in \mathcal{G}_k X.
    19-/
    20
    21namespace Lax606786.BernsteinNumberProperties
    22
    23open Lax606786.BanachGrassmannian Lax606786.OperatorStatistics
    24
    25variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    26
    27/-- `ρ_k(T) ≥ 0`. -/
    28axiom bernsteinNumber_nonneg (T : X →L[ℝ] X) (k : ℕ) : 0 ≤ bernsteinNumber T k
    29
    30/-- `ρ_0(T) = 0`. -/
    31axiom bernsteinNumber_zero (T : X →L[ℝ] X) : bernsteinNumber T 0 = 0
    32
    33/-- `ρ_1(T) = ‖T‖`. -/
    34axiom bernsteinNumber_one (T : X →L[ℝ] X) : bernsteinNumber T 1 = ‖T‖
    35
    36/-- `ρ_k(T) ≤ ‖T‖`. -/
    37axiom bernsteinNumber_le_opNorm (T : X →L[ℝ] X) (k : ℕ) : bernsteinNumber T k ≤ ‖T‖
    38
    39/-- `ρ_q(T) ≤ ρ_p(T)` for `1 ≤ p ≤ q`. -/
    40axiom bernsteinNumber_antitone (T : X →L[ℝ] X) {p q : ℕ} (hp : 1 ≤ p) (hpq : p ≤ q) :
    41 bernsteinNumber T q ≤ bernsteinNumber T p
    42
    43/-- `g(T, V) ≤ ρ_m(T)` for `V ∈ 𝒢_m X`. -/
    44axiom growth_le_bernsteinNumber {m : ℕ} (T : X →L[ℝ] X) (V : GrassmannianFin X m) :
    45 growth T (V.1 : Submodule ℝ X) ≤ bernsteinNumber T m
    46
    47/-- `ρ_1(T) ⋯ ρ_k(T) ≤ ‖T‖^k`. -/
    48axiom prod_bernsteinNumber_le_opNorm_pow (T : X →L[ℝ] X) (k : ℕ) :
    49 ∏ i ∈ Finset.range k, bernsteinNumber T (i + 1) ≤ ‖T‖ ^ k
    50
    51/-- `ρ_k(S ∘ T) ≤ ρ_k(S) ‖T‖`. -/
    52axiom bernsteinNumber_comp_le_mul_norm (S T : X →L[ℝ] X) (k : ℕ) :
    53 bernsteinNumber (S.comp T) k ≤ bernsteinNumber S k * ‖T‖
    54
    55/-- `ρ_k(S ∘ T) ≤ ‖S‖ ρ_k(T)`. -/
    56axiom bernsteinNumber_comp_le_norm_mul (S T : X →L[ℝ] X) (k : ℕ) :
    57 bernsteinNumber (S.comp T) k ≤ ‖S‖ * bernsteinNumber T k
    58
    59/-- `(T, V) ↦ g(T, V)` is continuous on `𝓑(X) × 𝒢_k X`. -/
    60axiom continuous_growth (k : ℕ) [NeZero k] :
    61 Continuous (fun p : (X →L[ℝ] X) × GrassmannianFin X k => growth p.1 (p.2.1 : Submodule ℝ X))
    62
    63end Lax606786.BernsteinNumberProperties
    64
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow 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…