Elementary properties of the growth function

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

proven

Loading review…

Natural Language Statement

Theorem

Let $X, Y, Z$ be real normed spaces, $T : X \to Y$ and $S : Y \to Z$ bounded operators and $V \le X$ a subspace. Then

$0 \le g(T, V) \le \|T\|$ , and $g(T, V)\,\|x\| \le \|Tx\|$ for every $x \in V$ ;
$g(T, V) \le g(T, W)$ whenever $0 \ne W \le V$ ;
$g(T, \operatorname{span}\{u\}) = \|Tu\|$ for every unit vector $u$ (for $T : X \to X$ );
(the growth inequality) $g(T, V)\, g(S, TV) \le g(ST, V) \le \min\bigl(\|T\|\, g(S, TV),\ g(T, V)\,\|S\|\bigr).$

Concept map

3 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

In the paper

page 3 of this submission's paper

Lean source view on GitLab

Show types on hover

1	import Lax606786.OperatorStatistics
2
3	/-!
4	---
5	title: Elementary properties of the growth function
6	type: theorem
7	---
8	Let $X, Y, Z$ be real normed spaces, $T : X \to Y$ and $S : Y \to Z$ bounded operators and
9	$V \le X$ a subspace. Then
10
11	- $0 \le g(T, V) \le \\|T\\|$ , and $g(T, V)\,\\|x\\| \le \\|Tx\\|$ for every $x \in V$ ;
12	- $g(T, V) \le g(T, W)$ whenever $0 \ne W \le V$ ;
13	- $g(T, \operatorname{span}\{u\}) = \\|Tu\\|$ for every unit vector $u$ (for $T : X \to X$ );
14	- (the growth inequality)
15	$g(T, V)\, g(S, TV) \le g(ST, V) \le \min\bigl(\\|T\\|\, g(S, TV),\ g(T, V)\,\\|S\\|\bigr).$
16	-/
17
18	namespace Lax606786.GrowthFunctionProperties
19
20	open Lax606786.OperatorStatistics
21
22	variable {X Y Z : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
23	[NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup Z] [NormedSpace ℝ Z]
24
25	/-- `g(T, V) ≥ 0`. -/
26	axiom growth_nonneg (T : X →L[ℝ] Y) (V : Submodule ℝ X) : 0 ≤ growth T V
27
28	/-- `g(T, V) ≤ ‖T‖`. -/
29	axiom growth_le_opNorm (T : X →L[ℝ] Y) (V : Submodule ℝ X) : growth T V ≤ ‖T‖
30
31	/-- `g(T, V) ‖u‖ ≤ ‖T u‖` for `u ∈ V`. -/
32	axiom growth_mul_norm_le (T : X →L[ℝ] Y) {V : Submodule ℝ X} {u : X} (hu : u ∈ V) :
33	growth T V * ‖u‖ ≤ ‖T u‖
34
35	/-- Shrinking the subspace can only increase the slowest growth. -/
36	axiom growth_le_growth {T : X →L[ℝ] X} {W V : Submodule ℝ X} (hWV : W ≤ V) (hW : W ≠ ⊥) :
37	growth T V ≤ growth T W
38
39	/-- The growth on a line is the growth of its unit vector. -/
40	axiom growth_span_singleton (T : X →L[ℝ] X) {u : X} (hu : ‖u‖ = 1) :
41	growth T (Submodule.span ℝ {u}) = ‖T u‖
42
43	/-- The growth inequality for a composition. -/
44	axiom growth_comp_bounds (T : X →L[ℝ] Y) (S : Y →L[ℝ] Z) (V : Submodule ℝ X) :
45	growth T V * growth S (V.map (T : X →ₗ[ℝ] Y)) ≤ growth (S.comp T) V ∧
46	growth (S.comp T) V ≤ min (‖T‖ * growth S (V.map (T : X →ₗ[ℝ] Y))) (growth T V * ‖S‖)
47
48	end Lax606786.GrowthFunctionProperties
49

Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Builds on

Lax606786.OperatorStatistics

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…

Lax Lean Archive

Elementary properties of the growth function

Flags

Flag this concept

Natural Language Statement

Theorem

1 `growth_comp_bounds` proven

2 `growth_le_growth` proven

3 `growth_le_opNorm` proven

4 `growth_mul_norm_le` proven

5 `growth_nonneg` proven

6 `growth_span_singleton` proven

In the paper

Lean source view on GitLab

Discussion

Settings