Measurability of the return time and the return-time exponent ratio

This module records two measurability facts about the suspension cross-section schedule that are needed to make the special-flow Lyapunov exponent set measurable in the base point. Both are read off mechanically from existing measurability infrastructure.

The first is that, for each lap index n, the return time returnTime T hτ n x (the flow time elapsed over n base returns) is a measurable function of the base point x. By definition returnTime T hτ n x = roofSum T hτ (n : ℤ) x = -(suspensionAct T hτ (n : ℤ) (x, 0)).2, so this follows from the measurability of the integer iterates of the suspension action (measurable_suspensionAct, of Oseledets.Continuous.SuspensionFlowMP).

The second is that the return-time exponent ratio x ↦ Real.log ‖cocycle A (⇑T) n x‖ / returnTime T hτ n x is measurable, combining the measurability of the discrete log-norm cocycle (measurable_logNorm_cocycle, of Oseledets.Cocycle.FurstenbergKesten) with the measurability of the return time. This is the per-index input to MeasureTheory.measurableSet_tendsto, which downstream turns the discrete return-time exponent convergence set into a measurable set.

Main results

• Oseledets.measurable_returnTime: the return time x ↦ returnTime T hτ n x is measurable.
• Oseledets.measurable_logNorm_div_returnTime: the return-time exponent ratio x ↦ Real.log ‖cocycle A (⇑T) n x‖ / returnTime T hτ n x is measurable.

theorem Oseledets.measurable_returnTime {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℕ) : Measurable fun (x : X) => returnTime T hτ n x

Measurability of the return time. For each lap index n, the flow time returnTime T hτ n x elapsed over n base returns is a measurable function of the base point x. It is the negated ℝ-coordinate of the n-th integer iterate of the suspension action started at height 0 (returnTime T hτ n x = -(suspensionAct T hτ (n : ℤ) (x, 0)).2), so it is measurable by measurable_suspensionAct.

theorem Oseledets.measurable_logNorm_div_returnTime {X : Type u_1} [MeasurableSpace X] {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℕ) : Measurable fun (x : X) => Real.log ‖cocycle A (⇑T) n x‖ / returnTime T hτ n x

Measurability of the return-time exponent ratio. For each lap index n, the rescaled log-norm x ↦ Real.log ‖cocycle A (⇑T) n x‖ / returnTime T hτ n x is a measurable function of the base point x. It is the quotient of the measurable discrete log-norm cocycle (measurable_logNorm_cocycle) and the measurable return time (measurable_returnTime). This is the per-index input to MeasureTheory.measurableSet_tendsto.