Sums of Lyapunov exponents, sign/vanishing, and the telescoping identity

This module is purely additive on top of the spectrum object Oseledets.exponents : Fin d → ℝ (defined in Oseledets/Lyapunov/Spectrum.lean) — the sorted, antitone, with-multiplicity Lyapunov spectrum of an ergodic, invertible, log-integrable matrix cocycle (standing hypotheses hT : Ergodic T μ, hA : ∀ x, (A x).det ≠ 0, hAmeas : Measurable A, hint : IntegrableLogNorm A μ, hint' : IntegrableLogNorm (fun x => (A x)⁻¹) μ, together with [IsProbabilityMeasure μ]).

It records three things requested as additive extensions:

• Exponent sums (sumPosExp, sumNonnegExp, sumNegExp, sumAllExp): the sums of the strictly positive / non-negative / strictly negative / all exponents, counted with multiplicity. These are plain real numbers. Because exponents is deterministic (it does not depend on the point x), these sums are deterministic constants; in particular they are trivially almost-everywhere constant, so no further ergodic argument is needed to identify them as a.e.-limits.
• Sign and vanishing characterizations (sumPosExp_nonneg, sumPosExp_eq_zero_iff, sumPosExp_pos_iff, and the dual statements for sumNegExp): immediate consequences of the definitions and the sign of the filtered summands.
• The telescoping identity (gammaK_eq_sum_top_exponents): the genuine ergodic growth rate Γ_k = lim (1/n) log sprod_k of the product of the top-k singular values equals the sum ∑_{i<k} exponents i of the top-k exponents. This is the shared foundation for the exterior characterization and the determinant identity.

Main definitions

• Oseledets.sumPosExp — sum of the strictly positive exponents (with multiplicity).
• Oseledets.sumNonnegExp — sum of the non-negative exponents (with multiplicity).
• Oseledets.sumNegExp — sum of the strictly negative exponents (with multiplicity).
• Oseledets.sumAllExp — sum of all exponents (with multiplicity).
• Oseledets.gammaK — the genuine ergodic growth rate Γ_k, the a.e.-constant limit of (1/n) log sprod_k, packaged as a plain real via Classical.choose.

Main results

• Oseledets.sumPosExp_nonneg, Oseledets.sumPosExp_eq_zero_iff, Oseledets.sumPosExp_pos_iff — sign/vanishing for the positive-exponent sum.
• Oseledets.sumNegExp_nonpos, Oseledets.sumNegExp_eq_zero_iff, Oseledets.sumNegExp_neg_iff — the dual contraction statements.
• Oseledets.gammaK_tendsto — gammaK k is the a.e. limit of (1/n) log sprod_k.
• Oseledets.gammaK_eq_sum_top_exponents — the telescoping identity Γ_k = ∑_{i<k} exponents i.

References

• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

noncomputable def Oseledets.sumPosExp {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : ℝ

Sum of the strictly positive Lyapunov exponents (counted with multiplicity). It is a plain real number; since exponents is deterministic this sum does not depend on the point x, hence is trivially almost-everywhere constant.

Equations

• Oseledets.sumPosExp hT hA hAmeas hint hint' = ∑ i : Fin d with 0 < Oseledets.exponents hT hA hAmeas hint hint' i, Oseledets.exponents hT hA hAmeas hint hint' i

noncomputable def Oseledets.sumNonnegExp {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : ℝ

Sum of the non-negative Lyapunov exponents (counted with multiplicity). It is a plain real number; since exponents is deterministic this sum does not depend on the point x, hence is trivially almost-everywhere constant.

Equations

• Oseledets.sumNonnegExp hT hA hAmeas hint hint' = ∑ i : Fin d with 0 ≤ Oseledets.exponents hT hA hAmeas hint hint' i, Oseledets.exponents hT hA hAmeas hint hint' i

noncomputable def Oseledets.sumNegExp {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : ℝ

Sum of the strictly negative Lyapunov exponents (counted with multiplicity). It is a plain real number; since exponents is deterministic this sum does not depend on the point x, hence is trivially almost-everywhere constant.

Equations

• Oseledets.sumNegExp hT hA hAmeas hint hint' = ∑ i : Fin d with Oseledets.exponents hT hA hAmeas hint hint' i < 0, Oseledets.exponents hT hA hAmeas hint hint' i

noncomputable def Oseledets.sumAllExp {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : ℝ

Sum of all Lyapunov exponents (counted with multiplicity). It is a plain real number; since exponents is deterministic this sum does not depend on the point x, hence is trivially almost-everywhere constant.

Equations

• Oseledets.sumAllExp hT hA hAmeas hint hint' = ∑ i : Fin d, Oseledets.exponents hT hA hAmeas hint hint' i

Sign and vanishing characterizations

theorem Oseledets.sumPosExp_nonneg {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : 0 ≤ sumPosExp hT hA hAmeas hint hint'

The positive-exponent sum is non-negative. Every summand is strictly positive on the filter, so the sum is ≥ 0.

theorem Oseledets.sumPosExp_eq_zero_iff {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : sumPosExp hT hA hAmeas hint hint' = 0 ↔ ∀ (i : Fin d), exponents hT hA hAmeas hint hint' i ≤ 0

Vanishing of the positive-exponent sum. The sum of the strictly positive exponents is zero iff there is no positive exponent, i.e. the cocycle is non-expanding (all exponents are ≤ 0).

theorem Oseledets.sumPosExp_pos_iff {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : 0 < sumPosExp hT hA hAmeas hint hint' ↔ ∃ (i : Fin d), 0 < exponents hT hA hAmeas hint hint' i

Positivity of the positive-exponent sum. The sum of the strictly positive exponents is strictly positive iff at least one exponent is positive.

theorem Oseledets.sumNegExp_nonpos {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : sumNegExp hT hA hAmeas hint hint' ≤ 0

The negative-exponent sum is non-positive. Every summand is strictly negative on the filter, so the sum is ≤ 0.

theorem Oseledets.sumNegExp_eq_zero_iff {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : sumNegExp hT hA hAmeas hint hint' = 0 ↔ ∀ (i : Fin d), 0 ≤ exponents hT hA hAmeas hint hint' i

Vanishing of the negative-exponent sum. The sum of the strictly negative exponents is zero iff there is no negative exponent, i.e. the cocycle is non-contracting (all exponents are ≥ 0).

theorem Oseledets.sumNegExp_neg_iff {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) : sumNegExp hT hA hAmeas hint hint' < 0 ↔ ∃ (i : Fin d), exponents hT hA hAmeas hint hint' i < 0

Negativity of the negative-exponent sum. The sum of the strictly negative exponents is strictly negative iff at least one exponent is negative.

The telescoping identity Γ_k = ∑_{i<k} exponents i

noncomputable def Oseledets.gammaK {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) {k : ℕ} (hk : k ≤ d) : ℝ

The genuine ergodic growth rate Γ_k, the μ-a.e.-constant limit of (1/n) log sprod_k (the product of the top-k singular values), packaged as a plain real via Classical.choose of tendsto_gammaK_of_integrableLogNorm. Defined for k ≤ d.

Equations

• Oseledets.gammaK hT hA hAmeas hint hint' hk = Classical.choose ⋯

theorem Oseledets.gammaK_tendsto {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) {k : ℕ} (hk : k ≤ d) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (sprod A T k n x)) Filter.atTop (nhds (gammaK hT hA hAmeas hint hint' hk))

The defining a.e. limit of gammaK: (1/n) log sprod_k → Γ_k for μ-a.e. x.

theorem Oseledets.gammaK_eq_sum_top_exponents {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {μ : MeasureTheory.Measure X} {T : X → 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)⁻¹) μ) {k : ℕ} (hk : k ≤ d) : gammaK hT hA hAmeas hint hint' hk = ∑ i : Fin k, exponents hT hA hAmeas hint hint' (Fin.castLE hk i)

The telescoping identity. The genuine ergodic growth rate Γ_k of the product of the top-k singular values equals the sum of the top-k Lyapunov exponents (with multiplicity): Γ_k = ∑_{i<k} exponents i. The top-k indices are realized as Fin.castLE hk : Fin k → Fin d.

Proof: (1/n) log sprod_k = ∑_{i<k} (1/n) log σᵢ (since sprod_k = ∏_{i<k} σᵢ, by Real.log_prod on the positive singular values), each term converges to exponents i by exponents_tendsto_log_singularValue, the finite sum of convergents converges to the sum of the limits (tendsto_finset_sum), and the limit is identified with Γ_k by uniqueness of limits against gammaK_tendsto.