Two-sided bounds for the log-growth of cocycle iterates on flag strata

For an ergodic cocycle A⁽ⁿ⁾ = cocycle A T n of invertible matrices over (X, μ, T), this file controls the normalized log-growth sequence n ↦ (1/n) log‖A⁽ⁿ⁾ v‖ of a vector v lying on a stratum of the Oseledets flag (v ∈ vflag A T x i.castSucc, v ∉ vflag A T x i.succ). Together with the per-vector limsup upper bound, the results here are the inputs of Oseledets.tendsto_inv_mul_log_norm_cocycle_apply_of_upper_lower (in Oseledets.Lyapunov.FiltrationInterfaceReduction), which upgrades them to the exact growth limit specList A T x i on each stratum.

Main results

• Oseledets.isBoundedUnder_log_norm_cocycle_apply: almost everywhere, for every v ≠ 0, the sequence (1/n) log‖A⁽ⁿ⁾ v‖ is bounded above and below, squeezed between the two convergent Furstenberg–Kesten envelopes (1/n) log‖A⁽ⁿ⁾‖ + (1/n) log‖v‖ and -(1/n) log‖(A⁽ⁿ⁾)⁻¹‖ + (1/n) log‖v‖.
• Oseledets.isBoundedUnder_inv_mul_log_norm_cocycle_apply_of_mem_stratum: the same two-sided boundedness for every stratum vector of the Oseledets flag (such a vector is automatically nonzero).
• Oseledets.specList_le_liminf_inv_mul_log_norm_cocycle_apply_of_bandProjector: the per-vector liminf lower bound specList A T x i ≤ liminf (1/n) log‖A⁽ⁿ⁾ v‖, derived from a band-projector convergence hypothesis via Oseledets.log_le_liminf_log_cocycle_apply.
• Oseledets.tendsto_inv_mul_log_norm_cocycle_apply_of_bandProjector: the exact per-vector growth limit, combining the limsup upper bound, the two-sided boundedness, and the liminf lower bound.

Helper norm bounds (apply-norm sandwiched by operator norm)

theorem Oseledets.norm_toEuclideanLin_cocycle_le {X : Type u_1} {d : ℕ} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (n : ℕ) (x : X) (v : EuclideanSpace ℝ (Fin d)) : ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖ ≤ ‖cocycle A T n x‖ * ‖v‖

‖A⁽ⁿ⁾ v‖ ≤ ‖A⁽ⁿ⁾‖ * ‖v‖ (apply-norm bounded above by the operator norm).

theorem Oseledets.toEuclideanLin_inv_cocycle_apply {X : Type u_1} {d : ℕ} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (hA : ∀ (x : X), (A x).det ≠ 0) (n : ℕ) (x : X) (v : EuclideanSpace ℝ (Fin d)) : (Matrix.toEuclideanLin (cocycle A T n x)⁻¹) ((Matrix.toEuclideanLin (cocycle A T n x)) v) = v

The inverse cocycle is a left inverse of the cocycle on EuclideanSpace.

theorem Oseledets.norm_le_norm_inv_cocycle_mul {X : Type u_1} {d : ℕ} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (hA : ∀ (x : X), (A x).det ≠ 0) (n : ℕ) (x : X) (v : EuclideanSpace ℝ (Fin d)) : ‖v‖ ≤ ‖(cocycle A T n x)⁻¹‖ * ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖

‖v‖ ≤ ‖(A⁽ⁿ⁾)⁻¹‖ * ‖A⁽ⁿ⁾ v‖ (apply-norm bounded below via the inverse operator norm).

The two-sided boundedness from Furstenberg–Kesten

theorem Oseledets.isBoundedUnder_log_norm_cocycle_apply {X : Type u_1} {d : ℕ} [MeasurableSpace X] {T : X → 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 → (Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) ∧ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖

The normalized log-norm of v along the cocycle is eventually ≤ the convergent envelope (1/n) log‖A⁽ⁿ⁾‖ + (1/n) log‖v‖ and eventually ≥ the convergent envelope -(1/n) log‖(A⁽ⁿ⁾)⁻¹‖ + (1/n) log‖v‖. Both envelopes converge (Furstenberg–Kesten), so the middle sequence is bounded on both sides.

Two-sided boundedness on each stratum

theorem Oseledets.isBoundedUnder_inv_mul_log_norm_cocycle_apply_of_mem_stratum {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (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) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → (Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) ∧ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖

Two-sided boundedness from Furstenberg–Kesten. The two-sided IsBoundedUnder side-conditions of tendsto_inv_mul_log_norm_cocycle_apply_of_upper_lower hold almost everywhere for every stratum vector. On each stratum the vector is nonzero (0 lies in every flag level, so v ∉ vflag i.succ ⟹ v ≠ 0), and the log-growth sequence is squeezed between the two convergent Furstenberg–Kesten envelopes.

The per-vector liminf lower bound

The per-vector liminf lower bound rests on the analytic core log_le_liminf_log_cocycle_apply: at threshold c = e^{specList i} > 0, if the band projectors for (c, ∞) converge to a limit P with P v ≠ 0, then specList i = log c ≤ liminf …. The remaining IsCoboundedUnder (· ≥ ·) side-condition is the lower boundedness furnished by isBoundedUnder_inv_mul_log_norm_cocycle_apply_of_mem_stratum (a bounded-below sequence is cobounded-below).

The band-projector convergence datum (hP, hPv) is the spectral-band identification of vflag membership: v ∉ vflag i.succ says v has a nonzero component in the band at level ≥ specList i, i.e. P v ≠ 0 for the limit projector at threshold e^{specList i}. This identification appears as the hypothesis hband, discharged by any vflag-to-band lemma of this shape.

theorem Oseledets.specList_le_liminf_inv_mul_log_norm_cocycle_apply_of_bandProjector {X : Type u_1} {d : ℕ} [MeasurableSpace X] [NeZero d] {μ : MeasureTheory.Measure X} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (hA : ∀ (x : X), (A x).det ≠ 0) (hband : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → ∃ (P : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi (Real.exp (specList A T x i))).indicator 1) n x) Filter.atTop (nhds P) ∧ (Matrix.toEuclideanLin P) v ≠ 0) (hbdd : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → (Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) ∧ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) Filter.atTop fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → specList A T x i ≤ Filter.liminf (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop

Liminf lower bound from band-projector convergence. Given, a.e. and per stratum-vector, the band projector convergence datum at threshold e^{specList i} (hband) and the lower boundedness of the log-growth sequence (from isBoundedUnder_inv_mul_log_norm_cocycle_apply_of_mem_stratum), the per-vector lower bound specList i ≤ liminf … holds.

The cobounded-below side-condition of log_le_liminf_log_cocycle_apply is supplied by the same IsBoundedUnder (· ≥ ·) from isBoundedUnder_inv_mul_log_norm_cocycle_apply_of_mem_stratum (IsBoundedUnder.isCoboundedUnder_ge, using that atTop is NeBot).

The exact per-vector growth limit

theorem Oseledets.tendsto_inv_mul_log_norm_cocycle_apply_of_bandProjector {X : Type u_1} {d : ℕ} [MeasurableSpace X] [NeZero d] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (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)⁻¹) μ) (hub : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → Filter.limsup (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanLin (cocycle A T n x)) v‖) Filter.atTop ≤ specList A T x i) (hband : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → ∃ (P : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi (Real.exp (specList A T x i))).indicator 1) n x) Filter.atTop (nhds P) ∧ (Matrix.toEuclideanLin P) v ≠ 0) : ∀ᵐ (x : X) ∂μ, ∀ (i : Fin (specCard A T x)), ∀ v ∈ ↑(vflag A T x i.castSucc), v ∉ vflag A T x i.succ → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle A T n x)) v‖) Filter.atTop (nhds (specList A T x i))

The exact per-vector growth limit: given the limsup upper bound hub and the band-projector datum hband, the normalized log-growth sequence of every stratum vector converges to the corresponding exponent. This feeds isBoundedUnder_inv_mul_log_norm_cocycle_apply_of_mem_stratum and specList_le_liminf_inv_mul_log_norm_cocycle_apply_of_bandProjector into tendsto_inv_mul_log_norm_cocycle_apply_of_upper_lower.