The Grassmannian contraction estimate
Lax606786.GrassmannianContraction · concepts/Lax606786/GrassmannianContraction.lean · lax-606786
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let be a real normed space, , a bounded operator on and with . Let with and . Then and, writing ,
So an operator with a gap between and contracts the subspaces on which it grows fast (Lee 2024, Lemma 12).
Concept map
In the paper
- page 4 of this submission's paper
Lean source view on GitLab
| 1 | import Lax606786.OperatorStatistics |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: The Grassmannian contraction estimate |
| 6 | type: theorem |
| 7 | --- |
| 8 | Let be a real normed space, , a bounded operator on and with |
| 9 | . Let with and |
| 10 | . Then and, writing |
| 11 | , |
| 12 | |
| 13 | So an operator with a gap between and contracts the subspaces on which it |
| 14 | grows fast (Lee 2024, Lemma 12). |
| 15 | -/ |
| 16 | |
| 17 | namespace Lax606786.GrassmannianContraction |
| 18 | |
| 19 | open Lax606786.BanachGrassmannian Lax606786.OperatorStatistics |
| 20 | |
| 21 | /-- The images of two fast-growing `k`-dimensional subspaces are close. -/ |
| 22 | axiom 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 | |
| 32 | end Lax606786.GrassmannianContraction |
| 33 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments