The upper Lyapunov growth function

This module introduces the upper Lyapunov growth function

lambdaBar A T x v = limsup_n (1/n) · log ‖A⁽ⁿ⁾(x) · v‖,

the per-vector growth rate of the linear cocycle A over T. Here A⁽ⁿ⁾(x) · v is the action Matrix.toEuclideanCLM (cocycle A T n x) v of the cocycle iterate on the Euclidean vector v.

Main results

The key structural facts proved here, feeding the ultrametric machinery of Oseledets.Lyapunov.Ultrametric:

• lambdaBar_smul: lambdaBar is invariant under nonzero scaling of the vector (unconditional);
• lambdaBar_equivariant: A-equivariance lambdaBar A T x v = lambdaBar A T (T x) (A x·v);
• lambdaBar_mem_Icc: finiteness: for a.e. x, lambdaBar A T x v lies in a fixed interval [lamBot, lamTop] (the extremal Lyapunov exponents from Furstenberg–Kesten);
• lambdaBar_add_le, isUltrametricGrowth_lambdaBar: the non-Archimedean inequality and the packaged statement that for a.e. x the function lambdaBar A T x is an IsUltrametricGrowth function.

Implementation notes

The non-Archimedean step (and the equivariance reindexing) needs the defining sequence (1/n)·log‖A⁽ⁿ⁾(x)·v‖ to be bounded; boundedness holds a.e. by the Furstenberg–Kesten sandwich. Accordingly lambdaBar_add_le and lambdaBar_equivariant carry explicit IsBoundedUnder hypotheses on that sequence, while the almost-everywhere statement isUltrametricGrowth_lambdaBar discharges them from the Furstenberg–Kesten limits (via the private growthSeq_bounded). lambdaBar_smul is fully unconditional (the perturbation (1/n)·log|c| is uniformly bounded), proved through the helper limsup_eq_of_tendsto_sub_zero.

noncomputable def Oseledets.lambdaBar {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (v : EuclideanSpace ℝ (Fin d)) : ℝ

The upper Lyapunov growth function lambdaBar A T x v = limsup_n (1/n) log‖A⁽ⁿ⁾(x) v‖.

Equations

• Oseledets.lambdaBar A T x v = Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (Oseledets.cocycle A T n x)) v‖) Filter.atTop

theorem Oseledets.lambdaBar_eq_limsup_growthSeq {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (v : EuclideanSpace ℝ (Fin d)) : lambdaBar A T x v = Filter.limsup (Oseledets.growthSeq✝ A T x v) Filter.atTop

Nonzeroness and norm bridges

The per-n sandwich inequalities

Boundedness of the defining sequence (a.e., from Furstenberg–Kesten)

A robust limsup-invariance helper

limsup (along atTop in ℝ) is unchanged when the sequence is perturbed by a term that tends to 0, without any boundedness hypothesis. The proof works directly on the defining sets {a | ∀ᶠ n, u n ≤ a}: the vanishing perturbation makes these two sets have equal sInf (handling the empty/unbounded "junk-value" cases uniformly).

Scaling invariance

theorem Oseledets.lambdaBar_smul {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) {c : ℝ} (hc : c ≠ 0) (v : EuclideanSpace ℝ (Fin d)) (_hv : v ≠ 0) : lambdaBar A T x (c • v) = lambdaBar A T x v

Scaling invariance. lambdaBar is invariant under nonzero scaling of the vector.

A-equivariance

theorem Oseledets.lambdaBar_equivariant {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) (_hA : (A x).det ≠ 0) (v : EuclideanSpace ℝ (Fin d)) (_hv : v ≠ 0) (hbddA : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop (Oseledets.growthSeq✝ A T (T x) ((Matrix.toEuclideanCLM (A x)) v))) (hbddB : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop (Oseledets.growthSeq✝ A T (T x) ((Matrix.toEuclideanCLM (A x)) v))) : lambdaBar A T x v = lambdaBar A T (T x) ((Matrix.toEuclideanCLM (A x)) v)

A-equivariance. lambdaBar A T x v = lambdaBar A T (T x) (A x · v).

Boundedness of the target sequence growthSeq A T (T x) (A x·v) is required: the limsup of the (x,v) sequence is the limsup of the same log-data scaled by (n+1)⁻¹ instead of n⁻¹, and the two scalings differ by (1/(n+1) - 1/n)·log‖·‖ = -(n+1)⁻¹·(n⁻¹·log‖·‖), which tends to 0 exactly because n⁻¹·log‖·‖ is bounded. This boundedness holds a.e. by Furstenberg–Kesten and is supplied from growthSeq_bounded.

Finiteness via the Furstenberg–Kesten sandwich

theorem Oseledets.lambdaBar_mem_Icc {X : Type u_1} {T : X → X} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : ∃ (lamBot : ℝ) (lamTop : ℝ), lamBot ≤ lamTop ∧ ∀ᵐ (x : X) ∂μ, ∀ (v : EuclideanSpace ℝ (Fin d)), v ≠ 0 → lambdaBar A T x v ∈ Set.Icc lamBot lamTop

Finiteness. For a.e. x, every nonzero v has lambdaBar A T x v in a fixed interval [lamBot, lamTop] whose endpoints are the extremal (bottom/top) Lyapunov exponents from Furstenberg–Kesten.

The ultrametric (non-Archimedean) inequality

theorem Oseledets.lambdaBar_add_le {X : Type u_1} {T : X → X} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (x : X) {v w : EuclideanSpace ℝ (Fin d)} (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0) (hbv : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop (Oseledets.growthSeq✝ A T x v)) (hbv' : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop (Oseledets.growthSeq✝ A T x v)) (hbw : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop (Oseledets.growthSeq✝ A T x w)) (hbw' : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop (Oseledets.growthSeq✝ A T x w)) (hbvw' : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop (Oseledets.growthSeq✝ A T x (v + w))) : lambdaBar A T x (v + w) ≤ max (lambdaBar A T x v) (lambdaBar A T x w)

Ultrametric inequality. The non-Archimedean inequality, with boundedness of the three defining sequences (which holds a.e. by Furstenberg–Kesten; supplied via growthSeq_bounded in isUltrametricGrowth_lambdaBar).

Packaged ultrametric growth function (a.e.)

theorem Oseledets.isUltrametricGrowth_lambdaBar {X : Type u_1} {T : X → X} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : ∀ᵐ (x : X) ∂μ, IsUltrametricGrowth (lambdaBar A T x)

For a.e. x, the upper Lyapunov growth function lambdaBar A T x is an IsUltrametricGrowth function: scaling-invariant (lambdaBar_smul) and non-Archimedean (lambdaBar_add_le, with the required boundedness discharged from the Furstenberg–Kesten sandwich growthSeq_bounded).

A-equivariance, almost-everywhere form

theorem Oseledets.lambdaBar_equivariant_ae {X : Type u_1} {T : X → X} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : ∀ᵐ (x : X) ∂μ, ∀ (v : EuclideanSpace ℝ (Fin d)), v ≠ 0 → lambdaBar A T x v = lambdaBar A T (T x) ((Matrix.toEuclideanCLM (A x)) v)

A-equivariance (a.e.). For a.e. x, the growth function satisfies the clean equivariance lambdaBar A T x v = lambdaBar A T (T x) (A x · v) for every nonzero v, with the boundedness hypotheses of lambdaBar_equivariant discharged from the Furstenberg–Kesten sandwich. The boundedness is needed at the image point T x; it holds a.e. in x by pulling back (via T measure-preserving) the a.e. boundedness at a generic point delivered by growthSeq_bounded.