Regularity of the Lyapunov exponents in the generating cocycle #
The regularity of the Lyapunov exponents as functions of the generator A, built on
the spectrum object Oseledets.exponents : Fin d → ℝ, the telescoping growth rate
Oseledets.gammaK (Oseledets/Lyapunov/ExponentSums.lean), and the determinant identity
Oseledets.sumAllExp_eq_integral_log_abs_det (Oseledets/Lyapunov/DetIdentity.lean).
The Fekete infimum representation
Γ_k = ⨅ n, (∫ log sprod_k(n+1))/(n+1)(gammaK_eq_iInf). The normalized integral sequence is the average of a subadditive cocycle (isSubadditiveCocycle_logSprodintegrated over the measure-preserving base), so by Fekete's lemma it converges to the infimum of its values. The ergodic a.e.-constant limitgammaKcoincides with this infimum; the non-trivial direction of that coincidence is a two-sided Fatou argument (gammaK_eq_gammaKInf).Per-
nintegral continuity under a uniform log-integrable envelope (regime 1,tendsto_integral_logSprod_of_dominated). If a family of generatorsAₘ → Aconverges entrywise a.e. with‖Aₘ‖, ‖Aₘ⁻¹‖dominated by fixedL¹-log functions, then by dominated convergence∫ log sprod_k(Aₘ, n) → ∫ log sprod_k(A, n)for each fixedn. Pointwise generator convergence alone is insufficient: the dominated-convergence theorem needs a fixed integrable envelope, which is exactly what the uniformL¹-log hypothesis supplies.Upper semicontinuity of the partial sums and the top exponent (
gammaK_upperSemicontinuous,topExponent_upperSemicontinuous). An infimum of functions each continuous in the generator is upper semicontinuous; hence eachΓ_k(the sum of the top-kexponents) and the top exponentλ₁ = Γ_1are USC:limsup_m Γ_k(Aₘ) ≤ Γ_k(A). The positive-exponent summax_k Γ_kis then USC as a finite maximum of USC functions (a finitemaxoflimsups), assembled by the consumer fromgammaK_upperSemicontinuous.Lower semicontinuity of the bottom exponent (
botExp_lowerSemicontinuous). BecauseΓ_d = ∫ log|det|is continuous (in fact linear inlog|det|, see the determinant identity), and the bottom exponent isλ_d = Γ_d − Γ_{d-1}withΓ_{d-1}USC, the difference is lower semicontinuous.
Main definitions #
Oseledets.gammaKInf— the Fekete infimum⨅ n, (∫ log sprod_k(n+1))/(n+1).Oseledets.botExp— the bottom exponentλ_d = Γ_d − Γ_{d-1}.
Main results #
Oseledets.integral_logSprod_subadditive— the integral sequence is subadditive.Oseledets.tendsto_integral_logSprod— Fekete: the normalized integral sequence converges togammaKInf.Oseledets.gammaK_eq_gammaKInf,Oseledets.gammaK_eq_iInf— the ergodic constant is the Fekete infimum.Oseledets.tendsto_integral_logSprod_of_dominated— per-nintegral continuity under a fixed log-integrable envelope (regime 1).Oseledets.gammaK_upperSemicontinuous— USC of the top-kpartial-sum growth rateΓ_k.Oseledets.topExponent_upperSemicontinuous— USC of the top exponentλ₁ = Γ_1.Oseledets.botExp_eq_exponents_last,Oseledets.botExp_lowerSemicontinuous— the bottom exponent equals the smallest spectral value, and is lower semicontinuous.
Implementation notes #
- The partial sums
Γ_kand the positive-exponent sum are only upper semicontinuous, not continuous, in the generator. Full continuity of individual exponents fails in general: the spectrum can jump as a spectral gap closes. - An interior exponent
λᵢ = Γ_{i+1} − Γ_iis a difference of two USC functions, hence is in general neither USC nor LSC. The bottom exponent is the exception: it is LSC becauseΓ_dis continuous. - The semicontinuity statements assume the uniform or
L¹-log convergence regime with a fixed integrable envelope dominating‖Aₘ‖, ‖Aₘ⁻¹‖. Pointwise generator convergence alone does not suffice: the per-nintegral continuity step is a dominated-convergence argument that requires domination.
References #
- M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).
A Bochner–Fatou helper for nonnegative a.e.-convergent sequences #
If h n ≥ 0 (a.e.) is integrable, h n → H a.e. with H integrable, and the integral
sequence converges to b, then ∫ H ≤ b. This is Fatou's lemma in the convenient convergent
form; it powers the non-trivial direction of gammaK_eq_gammaKInf.
The Fekete infimum representation of Γ_k #
Subadditivity of the integral sequence. The sequence aₙ = ∫ log sprod_k(n) is
subadditive (a (m+n) ≤ a m + a n): integrate the subadditive-cocycle inequality
(isSubadditiveCocycle_logSprod) over the measure-preserving base. This is the Fekete input.
The Fekete infimum Γ_k = ⨅ n, (∫ log sprod_k(n+1))/(n+1). By Fekete's lemma the
normalized integral sequence of a subadditive sequence decreases to its infimum; this packages
that infimum as a plain real. (It is identified with the ergodic constant gammaK in
gammaK_eq_gammaKInf.)
Equations
Instances For
gammaKInf is the Subadditive.lim of the integral sequence. Both are sInf of the same
set (the image of Ici 1 under u · / ·); range_div_succ_eq reconciles the ⨅-over-ℕ
shifted indexing with the Subadditive.lim Ici 1 indexing.
Fekete's lemma. The normalized integral sequence (∫ log sprod_k(n+1))/(n+1) converges
to the Fekete infimum gammaKInf.
The ergodic constant equals the Fekete infimum #
The ergodic constant is the Fekete infimum. gammaK = gammaKInf. The
inequality gammaK ≤ gammaKInf is a Fatou estimate on f_n − L_n ≥ 0 where
L_n = −k·birkhoffAverage(log⁺‖A⁻¹‖) converges a.e. (Birkhoff) to a constant; the reverse
gammaKInf ≤ gammaK is the symmetric Fatou estimate on U_n − f_n ≥ 0 with
U_n = k·birkhoffAverage(log⁺‖A‖). The integral sequence converges to gammaKInf by Fekete
(tendsto_integral_logSprod), the integrands converge a.e. to gammaK (gammaK_tendsto), and
the dominating-Birkhoff integrals are constant by measure preservation.
The Fekete infimum representation of Γ_k. The ergodic growth
rate equals the infimum, over n, of the normalized integrals:
Γ_k = ⨅ n, (∫ log sprod_k(n+1))/(n+1). This is the representation that makes Γ_k an
infimum of functions continuous in the generator, hence upper semicontinuous.
Per-n integral continuity under a fixed log-integrable envelope (regime 1) #
Per-n integral continuity (dominated convergence, regime 1). Suppose a sequence of
generators B m → A is such that, for a fixed iterate count n and μ-a.e. x, the
integrand log sprod_k(B m, n, x) → log sprod_k(A, n, x) converges, and is dominated by a
fixed integrable function bound. Then ∫ log sprod_k(B m, n) → ∫ log sprod_k(A, n).
The a.e. integrand convergence is supplied, e.g., by entrywise a.e. convergence B m → A
through the continuity of the singular-value product sprod in the matrix entries; the fixed
bound (e.g. k·(log⁺‖·‖ + log⁺‖·⁻¹‖) for a uniform envelope) is the required L¹-log
domination. Pointwise generator convergence alone is insufficient: the dominated-convergence
theorem requires a fixed integrable envelope.
Upper semicontinuity of the partial sums, top exponent, and positive-exponent sum #
Upper semicontinuity of the partial sums in the generator. Let B i be a family of
generators (each satisfying the standing hypotheses, via hB) and A a limiting generator,
such that for every fixed n the per-n integral is continuous along the filter l
(hcont, the conclusion of tendsto_integral_logSprod_of_dominated). Then the partial-sum
growth rate Γ_k is upper semicontinuous: limsup_i Γ_k(B i) ≤ Γ_k(A).
This is upper semicontinuity, not continuity. Γ_k is an infimum of the
per-n continuous normalized integrals (gammaK_eq_iInf); an infimum of continuous functions is
USC, and the inequality can be strict — full continuity of the partial sums (and a fortiori of
individual exponents) fails in general when a spectral gap closes. The per-n continuity
hypothesis is the dominated-convergence conclusion and itself requires a fixed integrable
envelope (pointwise generator convergence alone does not suffice).
Upper semicontinuity of the top Lyapunov exponent. Specializing
gammaK_upperSemicontinuous to k = 1 (λ₁ = Γ_1): the top exponent is USC in the generator,
limsup_i λ₁(B i) ≤ λ₁(A). As for the partial sums, this is USC, not continuity.
Lower semicontinuity of the bottom exponent #
The bottom (smallest) Lyapunov exponent is λ_d = Γ_d − Γ_{d-1}. Since Γ_d = ∫ log|det| is
continuous (linear in log|det|, the determinant identity), while Γ_{d-1} is only USC, the
difference is lower semicontinuous — the opposite asymmetry to the top exponent.
The bottom Lyapunov exponent, as the telescoping difference Γ_d − Γ_{d-1}. By the
telescoping identity (gammaK_eq_sum_top_exponents) this equals the smallest entry of the
sorted spectrum exponents ⟨d-1, …⟩ (recorded in botExp_eq_exponents_last).
Equations
- Oseledets.botExp hT hA hAmeas hint hint' = Oseledets.gammaK hT hA hAmeas hint hint' ⋯ - Oseledets.gammaK hT hA hAmeas hint hint' ⋯
Instances For
The bottom exponent is the smallest entry of the sorted spectrum. Γ_d − Γ_{d-1}
telescopes to the last (smallest) spectral value exponents ⟨d-1, …⟩.
Lower semicontinuity of the bottom exponent in the generator. Under the per-n integral
continuity for the top-(d-1) sum (hcont, supplying USC of Γ_{d-1}) and continuity of the
determinant growth Γ_d = ∫ log|det| (hdet), the bottom exponent is lower semicontinuous:
botExp(A) ≤ liminf_i botExp(B i).
This LSC is the opposite asymmetry to the top exponent's USC, and is special
to the bottom exponent: it holds precisely because Γ_d = ∫ log|det| is continuous (indeed
linear) in the generator, whereas a generic interior exponent λᵢ = Γ_{i+1} − Γ_i is a
difference of two USC functions and has no semicontinuity in either direction.
Per-n integral continuity under a.e. generator convergence + uniform integrability #
(regime 2, the Vitali route)
The second per-n continuity regime replaces the fixed integrable envelope of regime 1
(tendsto_integral_logSprod_of_dominated) by the L¹-log control hypothesis of uniform
integrability of the integrand family log sprod_k(B m, n, ·), together with μ-a.e.
convergence of the generators B m → A. The latter is purely analytic: it propagates through
the cocycle (a finite matrix product / orbit composition), the Gram matrix, its sorted
eigenvalues (Weyl perturbation, tendsto_eigenvalues₀), the singular values
(gram_eigenvalues₀_eq_sq_singularValues), and finally sprod = ∏ σ and Real.log. This is the
a.e. convergence of log sprod in ae_tendsto_logSprod_of_ae_tendsto_generator. The integral
continuity is then Vitali's convergence theorem (tendsto_Lp_finite_of_tendsto_ae +
tendsto_integral_of_L1'), packaged in tendsto_integral_logSprod_of_unifIntegrable and combined
with the a.e. generator convergence in tendsto_integral_logSprod_of_ae_unifIntegrable.
Uniform integrability is an explicit hypothesis, not something
derived from pure L¹-log convergence of the generators: log sprod is not L¹-continuous in
posLog‖·‖, so pure L¹-log convergence of the generators does not imply integral continuity.
Uniform integrability is the correct L¹-log control that, together with a.e. convergence, makes
the Vitali theorem applicable. The a.e. generator-convergence helper requires
T to be measure-preserving: the integrand at x samples the generator along the finite
orbit x, Tx, …, T^{n-1}x, so propagating an a.e. statement from x to its orbit requires
quasi-measure-preservation of T. (At the wrapper's call site this is supplied by Ergodic.T.)
A.e. convergence of log sprod from a.e. generator convergence. If the
generators converge μ-a.e. B m → A, then for each fixed iterate count n and k ≤ d,
μ-a.e. the integrand converges log sprod_k(B m, n, x) → log sprod_k(A, n, x).
This is the analytic core of regime 2. The chain is: a.e. B m → A propagates to the cocycle
(ae_tendsto_cocycle_of_ae_tendsto_generator); the Gram matrix Qₙ = cocycleᵀ · cocycle
converges (continuity of transpose and matrix multiplication); its sorted eigenvalues converge
(Weyl perturbation, tendsto_eigenvalues₀); the squared singular values equal the Gram
eigenvalues (gram_eigenvalues₀_eq_sq_singularValues), so each σᵢ(B m)² → σᵢ(A)², hence
σᵢ(B m) → σᵢ(A) (Real.sqrt continuity, σᵢ ≥ 0); the finite product
sprod = ∏_{i<k} σᵢ converges (tendsto_finsetProd); and Real.log is continuous at the strictly
positive limit sprod_k(A, n, x) > 0 (sprod_pos).
The measure-preserving hypothesis hT is required: log sprod_k(·, n, x) samples the
generator along the finite orbit x, Tx, …, T^{n-1}x, so an a.e. statement at x propagates to
its orbit only through quasi-measure-preservation of T.
Per-n integral continuity via uniform integrability (Vitali, regime 2).
For a fixed iterate count n and k ≤ d, if the integrand family log sprod_k(B m, n, ·) is
uniformly integrable (hui), μ-a.e.-strongly-measurable (hBmeas), and converges μ-a.e. to
log sprod_k(A, n, ·) (hlim, with the limit L¹, hAmemLp), then the integrals converge:
∫ log sprod_k(B m, n) → ∫ log sprod_k(A, n).
This is Vitali's convergence theorem: a.e. convergence with uniform integrability yields
L¹-convergence (tendsto_Lp_finite_of_tendsto_ae), which gives integral convergence
(tendsto_integral_of_L1'). Uniform integrability is the L¹-log control replacing the
fixed envelope of regime 1; it is not derivable from pure L¹-log convergence of the
generators (log sprod is not L¹-continuous in posLog‖·‖) and is kept as a hypothesis.
Per-n integral continuity from a.e. generator convergence and uniform integrability.
Combines ae_tendsto_logSprod_of_ae_tendsto_generator (a.e. generator convergence B m → A ⟹
a.e. integrand convergence) with the Vitali theorem tendsto_integral_logSprod_of_unifIntegrable.
The output is exactly the per-n continuity hypothesis hcont consumed by
gammaK_upperSemicontinuous, topExponent_upperSemicontinuous,
and botExp_lowerSemicontinuous (those take hcont over any countably-generated NeBot filter,
and atTop on ℕ qualifies), so it feeds the regime-2 semicontinuity statement
gammaK_upperSemicontinuous_of_ae_unifIntegrable directly.
The measure-preserving hypothesis is supplied at the USC call site by Ergodic.toMeasurePreserving.
Uniform integrability remains an explicit hypothesis (the L¹-log control), not derived
from pure L¹-log convergence of the generators.
Regime-2 upper semicontinuity of the partial sums. Specializing gammaK_upperSemicontinuous
to the filter atTop on ℕ with the regime-2 per-n continuity from
tendsto_integral_logSprod_of_ae_unifIntegrable: under a.e.
generator convergence B m → A (hconv) and, for each fixed iterate count, a.e.-strong
measurability (hBmeas), an L¹ limit (hAmemLp), and uniform integrability (hui) of the
integrand family, the partial-sum growth rate Γ_k is upper semicontinuous:
limsup_m Γ_k(B m) ≤ Γ_k(A). Regime 2 thus feeds the same USC statement
gammaK_upperSemicontinuous.
This is upper semicontinuity, not continuity, and uniform integrability is an explicit
L¹-log hypothesis, not a consequence of pure L¹-log generator convergence.