Lax Lean Archive

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

Bernstein numbers under a projection

Lax606786.GrowthUnderProjections · concepts/Lax606786/GrowthUnderProjections.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 TT a bounded operator on XX.

    • (Small growth.) If V∈GkXV \in \mathcal{G}^k X, PP is a bounded projection onto VV and l≥1l \ge 1, then ρk+l(T)≤ρl(TP)\rho_{k+l}(T) \le \rho_l(TP).
    • (Large growth.) If V,V′∈GkXV, V' \in \mathcal{G}^k X, P,P′P, P' are bounded projections onto V,V′V, V', E=ker⁡PE = \ker P, P′T=TPP'T = TP, and g(T,E)>∥T∣V∥g(T, E) > \|T|_V\|, then for every ll,ρl(TP)≤4 ∥P∥ ∥P′∥ ρl+k(T).\rho_l(TP) \le 4\,\|P\|\,\|P'\|\,\rho_{l+k}(T).

    These are Lemmas 16 and 17 of Lee (2024).

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

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

    1 bernsteinNumber_add_le_comp_proj proven

    2 bernsteinNumber_comp_proj_le proven

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.OperatorStatistics
    2
    3/-!
    4---
    5title: Bernstein numbers under a projection
    6type: theorem
    7---
    8Let XX be a real normed space and TT a bounded operator on XX.
    9
    10- (Small growth.) If V∈GkXV \in \mathcal{G}^k X, PP is a bounded projection onto VV and
    11 l≥1l \ge 1, then ρk+l(T)≤ρl(TP)\rho_{k+l}(T) \le \rho_l(TP).
    12- (Large growth.) If V,V′∈GkXV, V' \in \mathcal{G}^k X, P,P′P, P' are bounded projections onto V,V′V, V',
    13 E=ker⁡PE = \ker P, P′T=TPP'T = TP, and g(T,E)>∥T∣V∥g(T, E) > \|T|_V\|, then for every ll,
    14 ρl(TP)≤4 ∥P∥ ∥P′∥ ρl+k(T).\rho_l(TP) \le 4\,\|P\|\,\|P'\|\,\rho_{l+k}(T).
    15
    16These are Lemmas 16 and 17 of Lee (2024).
    17-/
    18
    19namespace Lax606786.GrowthUnderProjections
    20
    21open Lax606786.BanachGrassmannian Lax606786.OperatorStatistics
    22
    23variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    24
    25/-- Compressing to a codimension-`k` subspace costs at most `k` Bernstein indices. -/
    26axiom bernsteinNumber_add_le_comp_proj (k l : ℕ) (hl : l ≠ 0) (V : GrassmannianCofin X k)
    27 (P : X →L[ℝ] X) (hP : ∀ x, P x ∈ (V.1.1 : Submodule ℝ X))
    28 (hidem : ∀ x ∈ (V.1.1 : Submodule ℝ X), P x = x) (T : X →L[ℝ] X) :
    29 bernsteinNumber T (k + l) ≤ bernsteinNumber (T.comp P) l
    30
    31/-- When `T` grows faster on `ker P` than on `range P`, compressing to `range P` loses at most
    32`k` Bernstein indices, up to the factor `4 ‖P‖ ‖P'‖`. -/
    33axiom bernsteinNumber_comp_proj_le (k l : ℕ) (V V' : GrassmannianCofin X k) (E : Submodule ℝ X)
    34 (P P' T : X →L[ℝ] X)
    35 (hPproj : LinearMap.IsProj (V.1.1 : Submodule ℝ X) (P : X →ₗ[ℝ] X))
    36 (hPker : LinearMap.ker (P : X →ₗ[ℝ] X) = E)
    37 (hP'proj : LinearMap.IsProj (V'.1.1 : Submodule ℝ X) (P' : X →ₗ[ℝ] X))
    38 (hPcompat : P'.comp T = T.comp P)
    39 (hfast : growth T E > ‖T.comp (V.1.1 : Submodule ℝ X).subtypeL‖) :
    40 bernsteinNumber (T.comp P) l ≤ 4 * ‖P‖ * ‖P'‖ * bernsteinNumber T (l + k)
    41
    42end Lax606786.GrowthUnderProjections
    43
    Show 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…