Lax Lean Archive

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

Growth, Bernstein numbers and the compactness seminorm of an operator

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

definition

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

    Definition

    Let T:X→YT : X \to Y be a bounded linear operator between real normed spaces.

    • The growth of TT on a subspace V⊆XV \subseteq X is the slowest growth of a unit vector of VV,g(T,V)=inf⁡x∈SV∥Tx∥,g(T, V) = \inf_{x \in \mathbb{S}_V} \|Tx\|,with the convention inf⁡∅=0\inf \emptyset = 0 (so g(T,{0})=0g(T, \{0\}) = 0).
    • For T:X→XT : X \to X and k≥0k \ge 0, the kk-th Bernstein number isρk(T)=sup⁡V∈GkXg(T,V).\rho_k(T) = \sup_{V \in \mathcal{G}_k X} g(T, V).In particular ρ1(T)=∥T∥\rho_1(T) = \|T\|, and ρk(T)=0\rho_k(T) = 0 when k>dim⁡Xk > \dim X.
    • The compactness seminorm of T:X→XT : X \to X is its distance to the compact operators,∥T∥c=inf⁡{∥T−K∥:K compact}.\|T\|_c = \inf \{\|T - K\| : K \text{ compact}\}.
    Concept map
    2 concepts; 8 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 2 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.Grassmannian
    2import Mathlib.Analysis.Normed.Operator.Compact.Basic
    3
    4/-!
    5---
    6title: Growth, Bernstein numbers and the compactness seminorm of an operator
    7type: definition
    8---
    9Let T:X→YT : X \to Y be a bounded linear operator between real normed spaces.
    10
    11- The **growth** of TT on a subspace V⊆XV \subseteq X is the slowest growth of a unit vector of
    12 VV,
    13 g(T,V)=inf⁡x∈SV∥Tx∥,g(T, V) = \inf_{x \in \mathbb{S}_V} \|Tx\|,
    14 with the convention inf⁡∅=0\inf \emptyset = 0 (so g(T,{0})=0g(T, \{0\}) = 0).
    15- For T:X→XT : X \to X and k≥0k \ge 0, the **kk-th Bernstein number** is
    16 ρk(T)=sup⁡V∈GkXg(T,V).\rho_k(T) = \sup_{V \in \mathcal{G}_k X} g(T, V).
    17 In particular ρ1(T)=∥T∥\rho_1(T) = \|T\|, and ρk(T)=0\rho_k(T) = 0 when k>dim⁡Xk > \dim X.
    18- The **compactness seminorm** of T:X→XT : X \to X is its distance to the compact operators,
    19 ∥T∥c=inf⁡{∥T−K∥:K compact}.\|T\|_c = \inf \{\|T - K\| : K \text{ compact}\}.
    20-/
    21
    22namespace Lax606786.OperatorStatistics
    23
    24open Lax606786.Grassmannian
    25
    26variable {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    27 [NormedAddCommGroup Y] [NormedSpace ℝ Y]
    28
    29/-- `g(T, V) = inf {‖T x‖ : x ∈ V, ‖x‖ = 1}`. -/
    30noncomputable def growth (T : X →L[ℝ] Y) (V : Submodule ℝ X) : ℝ :=
    31 sInf ((fun x : X => ‖T x‖) '' (Metric.sphere (0 : X) 1 ∩ (V : Set X)))
    32
    33/-- `ρ_k(T) = sup {g(T, V) : V ∈ 𝒢_k X}`. -/
    34noncomputable def bernsteinNumber (T : X →L[ℝ] X) (k : ℕ) : ℝ :=
    35 sSup (Set.range fun V : GrassmannianFin X k => growth T (V.1 : Submodule ℝ X))
    36
    37/-- `‖T‖_c = inf {‖T - K‖ : K compact}`. -/
    38noncomputable def compactSeminorm (T : X →L[ℝ] X) : ℝ :=
    39 sInf ((fun K : X →L[ℝ] X => ‖T - K‖) '' {K | IsCompactOperator K})
    40
    41end Lax606786.OperatorStatistics
    42
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…