The derivative (tangent) cocycle of a smooth self-map

For a differentiable self-map T : E → E of E := EuclideanSpace ℝ (Fin d), the family of derivatives x ↦ Dₓ T = fderiv ℝ T x is a linear cocycle over T: by the chain rule the derivative of the n-th iterate T^[n] factors as a product of derivatives along the orbit. Transporting fderiv ℝ T x : E →L[ℝ] E to a matrix through the star-algebra equivalence Matrix.toEuclideanCLM turns this into the matrix cocycle cocycle (derivativeCocycle T) T, which feeds directly into the Oseledets multiplicative ergodic theorem.

The matrix norm throughout is the (scoped) L2 operator norm Matrix.Norms.L2Operator; matrices act on EuclideanSpace ℝ (Fin d) via Matrix.toEuclideanCLM.

Main definitions

• Oseledets.derivativeCocycle — the matrix-valued generator x ↦ (toEuclideanCLM).symm (Dₓ T).

Main results

• Oseledets.toEuclideanCLM_derivativeCocycle — toEuclideanCLM (derivativeCocycle T x) = Dₓ T.
• Oseledets.norm_derivativeCocycle — the generator has the same L2 operator norm as Dₓ T.
• Oseledets.chainRule_cocycle — the chain-rule cocycle identity toEuclideanCLM (cocycle (derivativeCocycle T) T n x) = fderiv ℝ (T^[n]) x.
• Oseledets.measurable_derivativeCocycle — measurability of the generator from continuity of the second derivative data (here: from measurable_fderiv).
• Oseledets.det_derivativeCocycle_ne_zero — invertibility of each Dₓ T gives a nonvanishing matrix determinant for the generator.
• Oseledets.oseledets_filtration_derivativeCocycle — the Oseledets filtration specialized to the derivative cocycle of an ergodic differentiable map with integrable log-derivative data.

References

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

noncomputable def Oseledets.derivativeCocycle {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) : EuclideanSpace ℝ (Fin d) → Matrix (Fin d) (Fin d) ℝ

The derivative (tangent) cocycle generator of a self-map T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d): the matrix representing the Fréchet derivative fderiv ℝ T x, obtained by transporting Dₓ T : E →L[ℝ] E along the inverse of the star-algebra equivalence Matrix.toEuclideanCLM.

Equations

• Oseledets.derivativeCocycle T x = Matrix.toEuclideanCLM.symm (fderiv ℝ T x)

@[simp]

theorem Oseledets.toEuclideanCLM_derivativeCocycle {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) : Matrix.toEuclideanCLM (derivativeCocycle T x) = fderiv ℝ T x

The matrix derivativeCocycle T x represents the derivative fderiv ℝ T x.

theorem Oseledets.norm_derivativeCocycle {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) : ‖derivativeCocycle T x‖ = ‖fderiv ℝ T x‖

The generator has the same L2 operator norm as the derivative: ‖derivativeCocycle T x‖ equals ‖fderiv ℝ T x‖. This is the bridge identifying the matrix integrability hypotheses with the genuine log⁺‖Dₓ T‖ ones.

theorem Oseledets.chainRule_cocycle {d : ℕ} {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : Differentiable ℝ T) (n : ℕ) (x : EuclideanSpace ℝ (Fin d)) : Matrix.toEuclideanCLM (cocycle (derivativeCocycle T) T n x) = fderiv ℝ T^[n] x

Chain-rule cocycle identity. For a differentiable T, the matrix cocycle (derivativeCocycle T) T n x represents the derivative of the n-th iterate T^[n] at x. Proved by induction, peeling the innermost factor T from both the cocycle recursion (cocycle_succ) and the iterate (Function.iterate_succ, so T^[n+1] = T^[n] ∘ T).

theorem Oseledets.derivativeCocycle_apply {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (x : EuclideanSpace ℝ (Fin d)) (i j : Fin d) : derivativeCocycle T x i j = ((fderiv ℝ T x) (EuclideanSpace.single j 1)).ofLp i

The matrix entry (derivativeCocycle T x) i j is the i-th coordinate of Dₓ T applied to the j-th standard basis vector.

theorem Oseledets.measurable_derivativeCocycle {d : ℕ} (T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) : Measurable (derivativeCocycle T)

Measurability of the derivative cocycle generator. Each matrix entry is the (continuous) coordinate projection of x ↦ (fderiv ℝ T x) eⱼ, which is measurable by measurable_fderiv_apply_const.

theorem Oseledets.det_derivativeCocycle_ne_zero {d : ℕ} {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hiso : ∀ (x : EuclideanSpace ℝ (Fin d)), IsUnit (fderiv ℝ T x)) (x : EuclideanSpace ℝ (Fin d)) : (derivativeCocycle T x).det ≠ 0

If every derivative Dₓ T is invertible (as a continuous linear map), then the generator's determinant never vanishes. Invertibility transfers across the star-algebra equivalence toEuclideanCLM, and a matrix is a unit iff its determinant is.

theorem Oseledets.oseledets_filtration_derivativeCocycle {d : ℕ} {μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))} [MeasureTheory.IsProbabilityMeasure μ] {T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)} (hT : Ergodic T μ) (hdiff : Differentiable ℝ T) (hdet : ∀ (x : EuclideanSpace ℝ (Fin d)), (derivativeCocycle T x).det ≠ 0) (hint : IntegrableLogNorm (derivativeCocycle T) μ) (hint' : IntegrableLogNorm (fun (x : EuclideanSpace ℝ (Fin d)) => (derivativeCocycle T x)⁻¹) μ) : (∀ (n : ℕ) (x : EuclideanSpace ℝ (Fin d)), Matrix.toEuclideanCLM (cocycle (derivativeCocycle T) T n x) = fderiv ℝ T^[n] x) ∧ ∃ (k : ℕ) (lam : Fin k → ℝ) (V : Fin (k + 1) → EuclideanSpace ℝ (Fin d) → Submodule ℝ (EuclideanSpace ℝ (Fin d))), StrictAnti lam ∧ (∀ (i : Fin (k + 1)), MeasurableSubspace fun (x : EuclideanSpace ℝ (Fin d)) => V i x) ∧ ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂μ, V 0 x = ⊤ ∧ V (Fin.last k) x = ⊥ ∧ (∀ (i : Fin k), V i.succ x < V i.castSucc x) ∧ (∀ (i : Fin (k + 1)), Submodule.map (↑(Matrix.toEuclideanCLM (derivativeCocycle T x))) (V i x) = V i (T x)) ∧ ∀ (i : Fin k), ∀ v ∈ ↑(V i.castSucc x), v ∉ V i.succ x → Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (cocycle (derivativeCocycle T) T n x)) v‖) Filter.atTop (nhds (lam i))

Oseledets multiplicative ergodic theorem for the derivative cocycle. Let T be an ergodic measure-preserving differentiable self-map of EuclideanSpace ℝ (Fin d) with everywhere nonsingular derivative cocycle and integrable log-derivative data log⁺‖Dₓ T‖, log⁺‖(Dₓ T)⁻¹‖ ∈ L¹(μ). Then there is an A-equivariant Lyapunov filtration with the convergence (1/n) log‖D(T^[n]) v‖ → λᵢ along each stratum, for A := derivativeCocycle T.

The integrability hypotheses are stated directly for the matrix generator; by norm_derivativeCocycle these are exactly the genuine log⁺‖fderiv‖ (and inverse) conditions. The first conjunct records that the cocycle is the genuine tangent cocycle: each factor toEuclideanCLM (cocycle (derivativeCocycle T) T n x) is the derivative fderiv ℝ (T^[n]) x.