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

The Grassmannian contraction estimate

Lax606786.GrassmannianContraction · concepts/Lax606786/GrassmannianContraction.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, k≥1k \ge 1, TT a bounded operator on XX and Θ\Theta with ρk+1(T)<Θ<ρk(T)\rho_{k+1}(T) < \Theta < \rho_k(T). Let V,W∈GkXV, W \in \mathcal{G}_k X with g(T,V)>Θg(T, V) > \Theta and g(T,W)>Θg(T, W) > \Theta. Then TV,TW∈GkXTV, TW \in \mathcal{G}_k X and, writing x=ρk+1(T)/Θ∈[0,1)x = \rho_{k+1}(T)/\Theta \in [0, 1),

    d(TV,TW)≤4x1−x.d(TV, TW) \le \frac{4x}{1-x}.

    So an operator with a gap between ρk+1\rho_{k+1} and ρk\rho_k contracts the subspaces on which it grows fast (Lee 2024, Lemma 12).

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitLab

    1import Lax606786.OperatorStatistics
    2
    3/-!
    4---
    5title: The Grassmannian contraction estimate
    6type: theorem
    7---
    8Let XX be a real normed space, k≥1k \ge 1, TT a bounded operator on XX and Θ\Theta with
    9ρk+1(T)<Θ<ρk(T)\rho_{k+1}(T) < \Theta < \rho_k(T). Let V,W∈GkXV, W \in \mathcal{G}_k X with g(T,V)>Θg(T, V) > \Theta and
    10g(T,W)>Θg(T, W) > \Theta. Then TV,TW∈GkXTV, TW \in \mathcal{G}_k X and, writing
    11x=ρk+1(T)/Θ∈[0,1)x = \rho_{k+1}(T)/\Theta \in [0, 1),
    12d(TV,TW)≤4x1−x.d(TV, TW) \le \frac{4x}{1-x}.
    13So an operator with a gap between ρk+1\rho_{k+1} and ρk\rho_k contracts the subspaces on which it
    14grows fast (Lee 2024, Lemma 12).
    15-/
    16
    17namespace Lax606786.GrassmannianContraction
    18
    19open Lax606786.BanachGrassmannian Lax606786.OperatorStatistics
    20
    21/-- The images of two fast-growing `k`-dimensional subspaces are close. -/
    22axiom dist_image_le {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    23 (k : ℕ) [NeZero k] (T : X →L[ℝ] X) (Θ : ℝ)
    24 (hΘ : bernsteinNumber T (k + 1) < Θ) (hΘ' : Θ < bernsteinNumber T k)
    25 (V W : GrassmannianFin X k)
    26 (hV : Θ < growth T (V.1 : Submodule ℝ X)) (hW : Θ < growth T (W.1 : Submodule ℝ X))
    27 (TV TW : GrassmannianFin X k)
    28 (hTV : (TV.1 : Submodule ℝ X) = (V.1 : Submodule ℝ X).map (T : X →ₗ[ℝ] X))
    29 (hTW : (TW.1 : Submodule ℝ X) = (W.1 : Submodule ℝ X).map (T : X →ₗ[ℝ] X)) :
    30 dist TV TW ≤ 4 * (bernsteinNumber T (k + 1) / Θ) / (1 - bernsteinNumber T (k + 1) / Θ)
    31
    32end Lax606786.GrassmannianContraction
    33
    Show 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…