Between integer times: continuous growth equals integer-time growth

This file is the analysis core of the continuous-flow Oseledets multiplicative ergodic theorem (MET). It shows that the continuous-parameter exponential growth rate of a flow cocycle along a fixed direction agrees with the integer-time growth rate.

Concretely, fix a measure-preserving flow φ, a continuous-time linear cocycle A over φ, a point x, and a nonzero vector v. The integer-time growth n⁻¹ · log ‖A (n:ℝ) x · v‖ is governed by the discrete MET. The cocycle identity A t x = A r (φ (n:ℝ) x) · A (n:ℝ) x for t = r + n with n = ⌊t⌋₊ and r ∈ [0,1) together with two integrable controls of the one-step log-norm fluctuation (forward and inverse) lets one sandwich the continuous-time average between the integer-time average shifted by a vanishing error. A squeeze along the floor then transfers the integer-time limit L to the continuous-time limit.

Main results

• Oseledets.ae_tendsto_flowError_zero: the one-step fluctuation control evaluated along the integer orbit, n⁻¹ · (g (φ (n:ℝ) x) + g' (φ (n:ℝ) x)), tends to 0 almost everywhere.
• Oseledets.tendsto_log_norm_atTop_of_discrete: if the integer-time average n⁻¹ · log ‖A (n:ℝ) x v‖ converges to L and the fluctuation error vanishes, then the continuous-time average t⁻¹ · log ‖A t x v‖ converges to L as t → ∞.

Operator-norm bounds for toEuclideanCLM of a matrix

Error sublinearity along the integer orbit

theorem Oseledets.ae_tendsto_flowError_zero {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) {g g' : X → ℝ} (hg : MeasureTheory.Integrable g μ) (hg' : MeasureTheory.Integrable g' μ) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * (g (φ.toFun (↑n) x) + g' (φ.toFun (↑n) x))) Filter.atTop (nhds 0)

Error sublinearity, almost everywhere. For integrable controls g, g', the combined one-step fluctuation n⁻¹ · (g (φ (n:ℝ) x) + g' (φ (n:ℝ) x)) evaluated along the integer orbit of the flow tends to 0 for almost every x.

This is the orbital-tail estimate ae_tendsto_orbit_div_atTop_zero for the time-1 map of the flow, with the integer-time orbit (φ 1)^[n] x rewritten as φ (n:ℝ) x.

From the discrete limit to the continuous limit

theorem Oseledets.tendsto_log_norm_atTop_of_discrete {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (A : FlowCocycle φ d) {g g' : X → ℝ} (hgb : ∀ s ∈ Set.Icc 0 1, ∀ (y : X), ‖A.toFun s y‖.posLog ≤ g y) (hg'b : ∀ s ∈ Set.Icc 0 1, ∀ (y : X), ‖(A.toFun s y)⁻¹‖.posLog ≤ g' y) {x : X} {v : EuclideanSpace ℝ (Fin d)} (hv : v ≠ 0) {L : ℝ} (herr : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * (g (φ.toFun (↑n) x) + g' (φ.toFun (↑n) x))) Filter.atTop (nhds 0)) (hdisc : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (A.toFun (↑n) x)) v‖) Filter.atTop (nhds L)) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ * Real.log ‖(Matrix.toEuclideanCLM (A.toFun t x)) v‖) Filter.atTop (nhds L)

Crux: continuous growth equals integer-time growth. Fix a flow φ, a flow cocycle A, a point x, and a nonzero vector v. Suppose:

• g controls the forward one-step log-norm on [0,1] (Real.posLog ‖A s y‖ ≤ g y),
• g' controls the inverse one-step log-norm on [0,1] (Real.posLog ‖(A s y)⁻¹‖ ≤ g' y),
• the combined fluctuation error along the integer orbit vanishes (herr),
• the integer-time average n⁻¹ · log ‖A (n:ℝ) x v‖ converges to L (hdisc).

Then the continuous-time average t⁻¹ · log ‖A t x v‖ converges to L as t → ∞.

The proof writes t = r + n with n = ⌊t⌋₊ ≥ 1 and r ∈ [0,1), splits the cocycle via A t x = A r (φ (n:ℝ) x) · A (n:ℝ) x, and sandwiches log ‖A t x v‖ between a n ± (one-step control at φ (n:ℝ) x); dividing by t and squeezing along the floor delivers the limit.