Constructing SqueezeData for the Oseledets spectral upper bound #
This file builds a constructor SqueezeData.ofCore that takes the analytic limit and
boundedness facts about the cocycle along the orbit of x as inputs, and discharges all
the remaining (arithmetic or boundedness-from-convergence) fields of SqueezeData. The
analytic inputs are thereby isolated as the only substantial obligations; everything
routine is closed here.
Main results #
Oseledets.SqueezeData.ofCore: assemble aSqueezeDatafrom the core analytic inputs (the volume/determinant limits, the tempered angle, the factorizations, the per-direction lower bounds, the restriction bound, and the boundedness facts).Oseledets.spectral_upper_bound_of_core: the per-vector spectral upper boundlimsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ, obtained by composingSqueezeData.ofCorewithspectral_upper_bound_of_squeezeData.Oseledets.exists_dSum_tendsto_dExponent: almost-everywhere convergence of the determinant exponent(1/n) log |det A⁽ⁿ⁾|, supplying thehDfield ofSqueezeData.Oseledets.tendsto_angle_exponent_zero: the tempered-angle inputhS, derived fromL¹-integrability of the positive log of the inverse splitting angle.
References #
- L. Arnold, Random Dynamical Systems, Springer, 1998, §3.4.
- D. Ruelle, Ergodic theory of differentiable dynamical systems, Publ. Math. IHÉS 50 (1979), 27–58.
- S. Filip, Notes on the multiplicative ergodic theorem, Ergodic Theory Dynam. Systems 39 (2019), 1153–1189.
IsCoboundedUnder (·≤·) of a sequence follows from it being bounded below.
The determinant exponent hD #
sprod A T d n x = ∏_{i<d} σᵢ(A⁽ⁿ⁾) = |det A⁽ⁿ⁾|, so the determinant exponent is the top
Γ-limit Γ_d. This is the cleanest concrete field: it follows directly from the ergodic
Kingman limit tendsto_gammaK_of_integrableLogNorm at k = d, with no frame geometry
involved. It is exposed here as dExponent and exists_dSum_tendsto_dExponent.
For an ergodic T and an everywhere-invertible measurable cocycle generator with
integrable log-norms, the determinant exponent (1/n) log sprod_d(A⁽ⁿ⁾) → Γ_d for
μ-a.e. x (here sprod_d = ∏ all σ = |det|). This supplies the hD field of
SqueezeData, with dSum := Γ_d.
For v ≠ 0 and an invertible cocycle (det ≠ 0), the per-vector growth ‖A⁽ⁿ⁾ v‖ is
strictly positive at every n. This supplies the hMvpos field of SqueezeData.
The tempered angle hS via L¹-temperedness #
In general the image angle sin∠(A⁽ⁿ⁾F, A⁽ⁿ⁾S) between the fast and slow images converges
to a positive constant, not to 1. In the autonomous case S n = (1/n) log sin∠ → 0 simply
because sin∠ is eventually bounded below by a positive constant. In the general ergodic
case, equivariance A⁽ⁿ⁾S(x) = S(Tⁿx) together with the forward fast limit F gives
sin∠(A⁽ⁿ⁾F(x), A⁽ⁿ⁾S(x)) = θ(Tⁿx) for a fixed splitting-angle function θ : X → (0,1],
and (1/n) log θ(Tⁿx) → 0 follows from the L¹-temperedness hypothesis log(1/θ) ∈ L¹(μ)
(see Arnold §3.4 and Ruelle), discharged by tempering_posLog. Fischer's inequality
sin∠ ≤ 1 gives the upper side θ ≤ 1.
The lemma below derives hS from exactly this data: the equivariant representation
S n = (1/n) log (θ(Tⁿx)), the range 0 < θ ≤ 1, and the temperedness posLog(1/θ) ∈ L¹.
The tempered angle from L¹-temperedness. Suppose the angle sequence is the
orbit sample of a fixed splitting-angle function: S n = (n)⁻¹ · log (θ (Tⁿ x)) with
0 < θ y ≤ 1 for all y, and the temperedness y ↦ posLog ((θ y)⁻¹) ∈ L¹(μ). Then for
μ-a.e. x, S → 0. This is the precise content of the tempered angle, the hS field
of SqueezeData.
Core constructor for SqueezeData.
Takes the analytic inputs (the volume/determinant limits, the tempered angle, the
factorizations, the per-direction lower bounds, the restriction bound, and the
Furstenberg–Kesten-type boundedness facts) and assembles them into a SqueezeData. Each
hypothesis is named after the field it supplies; the coboundedness field hcobdd is
derived from the lower-boundedness hypothesis hMvlb.
This constructor isolates exactly the analytic content of the spectral upper bound.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The spectral upper bound from the core analytic inputs #
Composing SqueezeData.ofCore with spectral_upper_bound_of_squeezeData gives the
spectral upper bound directly from the analytic inputs: once they are supplied, the
per-vector spectral upper bound limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ follows with no
further work.
The per-vector spectral upper bound limsup (1/n) log ‖A⁽ⁿ⁾ v‖ ≤ λᵢ, assembled from
the core analytic inputs via SqueezeData.ofCore and
spectral_upper_bound_of_squeezeData.