Bounds on the growth rate of a vector

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

proven

Loading review…

Natural Language Statement

Theorem

Let $\mathcal{L}$ be a cocycle, $\omega \in \Omega$ and $x \in X$ , with growth rate $\lambda_\omega(x) = \limsup_n \frac1n \log\|\mathcal{L}^{(n)}_\omega x\|$ .

$\lambda_\omega(-x) = \lambda_\omega(x)$ , $\lambda_\omega(x + y) \le \max(\lambda_\omega(x), \lambda_\omega(y))$ , and $\lambda_\omega(x) = -\infty$ if $\mathcal{L}^{(n)}_\omega x = 0$ for some $n$ .
If $x \in W \setminus 0$ and $\frac1n \log g(\mathcal{L}^{(n)}_\omega, W) \to c$ , then $c \le \lambda_\omega(x)$ .
If $\|\mathcal{L}^{(n)}_\omega x\| \le K e^{cn}$ for all large $n$ , then $\lambda_\omega(x) \le c$ .
If $\lambda_\omega(x) < c$ , then $\|\mathcal{L}^{(n)}_\omega x\| < e^{cn}$ for all large $n$ .
If $x \in E$ and $\frac1n \log \|\mathcal{L}^{(n)}_\omega|_E\| \to c$ , then $\lambda_\omega(x) \le c$ .
If $E \in \mathcal{G}_m X$ with $m \ge 1$ , and both $\frac1n \log g(\mathcal{L}^{(n)}_\omega, E)$ and $\frac1n \log \|\mathcal{L}^{(n)}_\omega\|$ tend to a real number $\lambda$ , with $g(\mathcal{L}^{(n)}_\omega, E) > 0$ for large $n$ , then $\lambda_\omega(x) = \lambda$ for every nonzero $x \in E$ .

Concept map

6 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

Lean source view on GitLab

Show types on hover

1	import Lax606786.Cocycles
2	import Lax606786.BanachGrassmannian
3
4	/-!
5	---
6	title: Bounds on the growth rate of a vector
7	type: theorem
8	---
9	Let $\mathcal{L}$ be a cocycle, $\omega \in \Omega$ and $x \in X$ , with growth rate
10	$\lambda_\omega(x) = \limsup_n \frac1n \log\\|\mathcal{L}^{(n)}_\omega x\\|$ .
11
12	- $\lambda_\omega(-x) = \lambda_\omega(x)$ ,
13	$\lambda_\omega(x + y) \le \max(\lambda_\omega(x), \lambda_\omega(y))$ , and
14	$\lambda_\omega(x) = -\infty$ if $\mathcal{L}^{(n)}_\omega x = 0$ for some $n$ .
15	- If $x \in W \setminus 0$ and $\frac1n \log g(\mathcal{L}^{(n)}_\omega, W) \to c$ , then
16	$c \le \lambda_\omega(x)$ .
17	- If $\\|\mathcal{L}^{(n)}_\omega x\\| \le K e^{cn}$ for all large $n$ , then
18	$\lambda_\omega(x) \le c$ .
19	- If $\lambda_\omega(x) < c$ , then $\\|\mathcal{L}^{(n)}_\omega x\\| < e^{cn}$ for all large $n$ .
20	- If $x \in E$ and $\frac1n \log \\|\mathcal{L}^{(n)}_\omega\|_E\\| \to c$ , then
21	$\lambda_\omega(x) \le c$ .
22	- If $E \in \mathcal{G}_m X$ with $m \ge 1$ , and both
23	$\frac1n \log g(\mathcal{L}^{(n)}_\omega, E)$ and $\frac1n \log \\|\mathcal{L}^{(n)}_\omega\\|$ tend
24	to a real number $\lambda$ , with $g(\mathcal{L}^{(n)}_\omega, E) > 0$ for large $n$ , then
25	$\lambda_\omega(x) = \lambda$ for every nonzero $x \in E$ .
26	-/
27
28	namespace Lax606786.VectorGrowthRates
29
30	open Filter Topology
31	open Lax606786.Cocycles Lax606786.BanachGrassmannian Lax606786.OperatorStatistics
32	Lax606786.ExtendedLog
33
34	variable {Ω X : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω]
35	[NormedAddCommGroup X] [NormedSpace ℝ X] [MeasurableSpace X]
36
37	/-- An eventual exponential bound bounds the growth rate. -/
38	axiom lambdaAt_le_of_eventually_le (R : Cocycle Ω X) {ω : Ω} {x : X} {K c : ℝ}
39	(h : ∀ᶠ n : ℕ in atTop, ‖R.iterate n ω x‖ ≤ K * Real.exp (n * c)) :
40	R.lambdaAt ω x ≤ (c : EReal)
41
42	/-- A growth rate below `c` gives an eventual bound `e^{cn}`. -/
43	axiom eventually_lt_exp_of_lambdaAt_lt (R : Cocycle Ω X) {ω : Ω} {x : X} {c : ℝ}
44	(h : R.lambdaAt ω x < (c : EReal)) :
45	∀ᶠ n : ℕ in atTop, ‖R.iterate n ω x‖ < Real.exp (c * n)
46
47	/-- Vectors of a subspace grow no faster than the subspace's norm rate. -/
48	axiom lambdaAt_le_of_norm_tendsto (R : Cocycle Ω X) {ω : Ω} {E : Submodule ℝ X} {c : EReal}
49	(h : Tendsto (fun n : ℕ => logEReal ‖(R.iterate n ω).comp E.subtypeL‖ / (n : EReal)) atTop
50	(𝓝 c)) {x : X} (hx : x ∈ E) :
51	R.lambdaAt ω x ≤ c
52
53	/-- On a subspace growing uniformly at rate `λ`, every nonzero vector has rate `λ`. -/
54	axiom lambdaAt_eq_of_growth (R : Cocycle Ω X) {m : ℕ} [NeZero m] {lam : ℝ}
55	(E : Ω → GrassmannianFin X m) (ω : Ω)
56	(hgrow : Tendsto (fun n : ℕ =>
57	Real.log (growth (R.iterate n ω) ((E ω).1 : Submodule ℝ X)) / n) atTop (𝓝 lam))
58	(hnorm : Tendsto (fun n : ℕ => Real.log ‖R.iterate n ω‖ / n) atTop (𝓝 lam))
59	(hgpos : ∀ᶠ n : ℕ in atTop, 0 < growth (R.iterate n ω) ((E ω).1 : Submodule ℝ X))
60	{x : X} (hx : x ∈ ((E ω).1 : Submodule ℝ X)) (hx0 : x ≠ 0) :
61	R.lambdaAt ω x = (lam : EReal)
62
63	/-- `λ_ω(-x) = λ_ω(x)`. -/
64	axiom lambdaAt_neg (R : Cocycle Ω X) (ω : Ω) (x : X) : R.lambdaAt ω (-x) = R.lambdaAt ω x
65
66	/-- `λ_ω(x + y) ≤ max (λ_ω x) (λ_ω y)`. -/
67	axiom lambdaAt_add_le (R : Cocycle Ω X) (ω : Ω) (x y : X) :
68	R.lambdaAt ω (x + y) ≤ max (R.lambdaAt ω x) (R.lambdaAt ω y)
69
70	/-- A vector killed by some iterate has growth rate `-∞`. -/
71	axiom lambdaAt_eq_bot_of_iterate_eq_zero (R : Cocycle Ω X) {ω : Ω} {x : X} {n : ℕ}
72	(hx : R.iterate n ω x = 0) : R.lambdaAt ω x = ⊥
73
74	/-- A nonzero vector of `W` grows at least as fast as the slowest vector of `W`. -/
75	axiom le_lambdaAt_of_tendsto_growth (R : Cocycle Ω X) (ω : Ω) {W : Submodule ℝ X} {c : EReal}
76	(h : Tendsto (fun n : ℕ => logEReal (growth (R.iterate n ω) W) / (n : EReal)) atTop (𝓝 c))
77	{x : X} (hx : x ∈ W) (hx0 : x ≠ 0) : c ≤ R.lambdaAt ω x
78
79	end Lax606786.VectorGrowthRates
80

Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow 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…

Lax Lean Archive

Bounds on the growth rate of a vector

Flags

Flag this concept

Natural Language Statement

Theorem

1 `eventually_lt_exp_of_lambdaAt_lt` proven

2 `lambdaAt_add_le` proven

3 `lambdaAt_eq_bot_of_iterate_eq_zero` proven

4 `lambdaAt_eq_of_growth` proven

5 `lambdaAt_le_of_eventually_le` proven

6 `lambdaAt_le_of_norm_tendsto` proven

7 `lambdaAt_neg` proven

8 `le_lambdaAt_of_tendsto_growth` proven

Lean source view on GitLab

Discussion

Settings