Elementary properties of Bernstein numbers
Lax606786.BernsteinNumberProperties · concepts/Lax606786/BernsteinNumberProperties.lean · lax-606786
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let be a real normed space and bounded operators on .
- , , , and for .
- for every , and .
For every ,
Moreover, for the growth is jointly continuous in , for the operator norm on and the Hausdorff distance between unit spheres on .
Concept map
Evidence
This concept declares 10 statements. Each proof establishes one of them relative to its assumptions.
1 bernsteinNumber_antitone proven
2 bernsteinNumber_comp_le_mul_norm proven
3 bernsteinNumber_comp_le_norm_mul proven
4 bernsteinNumber_le_opNorm proven
5 bernsteinNumber_nonneg proven
6 bernsteinNumber_one proven
7 bernsteinNumber_zero proven
8 continuous_growth proven
9 growth_le_bernsteinNumber proven
10 prod_bernsteinNumber_le_opNorm_pow proven
In the paper
- page 4 of this submission's paper
Lean source view on GitLab
| 1 | import Lax606786.OperatorStatistics |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Elementary properties of Bernstein numbers |
| 6 | type: theorem |
| 7 | --- |
| 8 | Let be a real normed space and bounded operators on . |
| 9 | |
| 10 | - , , , and |
| 11 | for . |
| 12 | - for every , and |
| 13 | . |
| 14 | |
| 15 | For every , |
| 16 | |
| 17 | Moreover, for the growth is jointly continuous in , for the operator |
| 18 | norm on and the Hausdorff distance between unit spheres on . |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax606786.BernsteinNumberProperties |
| 22 | |
| 23 | open Lax606786.BanachGrassmannian Lax606786.OperatorStatistics |
| 24 | |
| 25 | variable {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] |
| 26 | |
| 27 | /-- `ρ_k(T) ≥ 0`. -/ |
| 28 | axiom bernsteinNumber_nonneg (T : X →L[ℝ] X) (k : ℕ) : 0 ≤ bernsteinNumber T k |
| 29 | |
| 30 | /-- `ρ_0(T) = 0`. -/ |
| 31 | axiom bernsteinNumber_zero (T : X →L[ℝ] X) : bernsteinNumber T 0 = 0 |
| 32 | |
| 33 | /-- `ρ_1(T) = ‖T‖`. -/ |
| 34 | axiom bernsteinNumber_one (T : X →L[ℝ] X) : bernsteinNumber T 1 = ‖T‖ |
| 35 | |
| 36 | /-- `ρ_k(T) ≤ ‖T‖`. -/ |
| 37 | axiom bernsteinNumber_le_opNorm (T : X →L[ℝ] X) (k : ℕ) : bernsteinNumber T k ≤ ‖T‖ |
| 38 | |
| 39 | /-- `ρ_q(T) ≤ ρ_p(T)` for `1 ≤ p ≤ q`. -/ |
| 40 | axiom 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`. -/ |
| 44 | axiom 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`. -/ |
| 48 | axiom 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‖`. -/ |
| 52 | axiom 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)`. -/ |
| 56 | axiom 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`. -/ |
| 60 | axiom continuous_growth (k : ℕ) [NeZero k] : |
| 61 | Continuous (fun p : (X →L[ℝ] X) × GrassmannianFin X k => growth p.1 (p.2.1 : Submodule ℝ X)) |
| 62 | |
| 63 | end Lax606786.BernsteinNumberProperties |
| 64 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments