The restricted Lyapunov exponent (two-sided MET) #
This module identifies the restricted Kingman constant of the restricted cocycle
restGen A V x = A x · P_{V x} on the forward Oseledets level V := Vᵢ with the
Lyapunov exponent λᵢ = expEnum lam0 d i, and derives the backward-orbit envelope
limsup (1/n) log ‖A⁽ⁿ⁾(T⁻ⁿx) · P_{Vᵢ(T⁻ⁿx)}‖ ≤ λᵢ (the ≤ direction is the only one
consumed downstream by the transversality crux ae_crux).
The architecture:
limsup_log_sum_le_max— for finitely many eventually-positive sequencesaⱼ,limsup (1/n) log (Σⱼ aⱼ n) ≤ maxⱼ limsup (1/n) log aⱼ n. Built from the one-sided helperlimsup_inv_mul_log_sum_le.exists_stratum— every nonzerov ∈ Vᵢ(x)lies in a stratumj ≥ iof the flag (pure order logic on theoseledets_filtration_dimsflag), so its growth rate≤ λᵢ.restricted_const_eq— the Kingman constantcofrestLog A V T(restLog_kingman) equalsλᵢ. Both bounds are evaluated at the base point through the floor-absorbed identityrestLog_eq_on_good: the≥direction uses a stratum witness, the≤direction the orthonormal-basis bound‖A⁽ⁿ⁾ · P‖ ≤ Σⱼ ‖A⁽ⁿ⁾ eⱼ‖(norm_mul_orthProj_le_sum) together withlimsup_log_sum_le_max.ae_limsup_restricted_backward_le— the backward-orbit envelope, obtained fromrestLog_backward_kingman, the floor absorption along the backward orbit (restLog_eq_on_good), andrestricted_const_eq.
A log-sum-max limsup bound #
Log-sum-max for limsups. For finitely many sequences a : s → ℕ → ℝ with
aⱼ n ≥ 0, each normalized log-limsup bounded above (IsBoundedUnder), eventually
positive total sum, the normalized log of the sum has limsup at most the maximum of the
individual limsups. This is the additive engine of the restricted-exponent upper bound;
it is built directly from limsup_inv_mul_log_sum_le and eventually_le_exp_of_limsup_le.
The orthonormal-basis norm bound #
Basis bound for the restricted operator. For a subspace K with orthonormal basis
e = stdOrthonormalBasis ℝ K, the restricted-operator norm is bounded by the sum of the
norms of the images of the basis vectors: ‖M · P_K‖ ≤ Σⱼ ‖M eⱼ‖. The proof bounds
‖(M·P_K) w‖ for unit w by expanding P_K w in the basis and using Bessel
(|⟪eⱼ, P_K w⟫| ≤ ‖w‖).
Flag descent and projection equivariance #
Stratum descent on the flag. In a decreasing flag from ⊤ to ⊥, every nonzero
vector v determines a stratum i : Fin k: the levels containing v are exactly those
of index ≤ i. (Order logic, identical to the one-sided Corollaries.exists_stratum.)
Map-equivariance promotes to projection conjugation. From the flag equivariance
map (toEuclideanCLM (A x)) (V x) = V (T x) follows the matrix identity
P_{V (T x)} · A x · P_{V x} = A x · P_{V x}: A x maps V x into V (T x), so the
projection P_{V (T x)} fixes the image of A x · P_{V x}.
Extracting measurable conull sets and forward-orbit a.e. facts #
A measurable conull set on which a given a.e. property holds.
From an a.e. property P, a.e. the property holds along the entire forward orbit
∀ k, P (T^[k] x). Uses measure-preservation of each iterate.
Convergence of a finite supremum of sequences #
The pointwise finite supremum of finitely many convergent sequences converges to the supremum of the limits.
The per-point bounds on the restricted growth #
Per-point lower bound. With the floor-absorbed restricted-growth limit hw and a
unit stratum witness v ∈ Vᵢ(x) whose unrestricted growth is lam, the restricted
constant c is at least lam: ‖A⁽ⁿ⁾ v‖ ≤ ‖A⁽ⁿ⁾ · P‖ since P v = v and v is a unit
vector.
Per-point upper bound. With the floor-absorbed restricted-growth limit hw, an
orthonormal basis eⱼ of Vᵢ(x), and each basis-vector growth Lⱼ ≤ lam, the restricted
constant c is at most lam. The proof bounds ‖A⁽ⁿ⁾ · P‖ ≤ Σⱼ ‖A⁽ⁿ⁾ eⱼ‖
(norm_mul_orthProj_le_sum), writes each summand as exp (n · gⱼ n), dominates the sum by
N · exp (n · maxⱼ gⱼ n), and concludes via le_of_tendsto_of_tendsto against the
majorant (1/n) log N + maxⱼ gⱼ n → maxⱼ Lⱼ.
Absorbed restricted-growth limit. On the good orbit (Vᵢ(x) ≠ ⊥ and the one-step
flag equivariance along the forward orbit), the floored restricted-log Kingman limit equals
the limit of the floor-absorbed restricted operator norm
(1/n) log ‖A⁽ⁿ⁾(x) · P_{Vᵢ(x)}‖. (restLog_eq_on_good for n ≥ 1.)
The restricted Kingman constant equals λᵢ, and the backward envelope #
The restricted Kingman constant equals λᵢ. For the forward Oseledets level
Vᵢ = V i.castSucc, the Kingman constant c of the restricted cocycle restLog A Vᵢ T
(the forward a.e. limit of (1/n) restLog n) equals the Lyapunov exponent
λᵢ = expEnum lam0 d i.
The ≥ direction uses a stratum witness v ∈ Vᵢ(x) ∖ Vᵢ₊₁(x) with growth exactly λᵢ;
the ≤ direction bounds ‖A⁽ⁿ⁾ · P_{Vᵢ}‖ by the sum of growths of an orthonormal basis of
Vᵢ(x), each basis vector lying in a stratum ≥ i (hence with growth ≤ λᵢ). Both bounds
are evaluated at the base point through the floor-absorbed identity (restLog_eq_on_good,
along the forward orbit made good by ae_forall_iterate_of_ae), and c is pinned down as a
constant via the a.e. Kingman limit.
The backward-orbit restricted envelope (the ≤ direction consumed by the
transversality crux ae_crux). For a.e. x, the floor-absorbed restricted operator
norm along the backward orbit has limsup at most λᵢ:
limsup (1/n) log ‖A⁽ⁿ⁾(T⁻ⁿ x) · P_{Vᵢ(T⁻ⁿ x)}‖ ≤ λᵢ.
Assembled from restLog_backward_kingman (the backward Kingman limit shares the forward
constant c), restricted_const_eq (c = λᵢ), and the floor absorption along the backward
orbit: the whole bi-orbit is good a.e. (ae_forall_iterate_of_ae over T.symm), so
restLog_eq_on_good absorbs the floor at each T⁻ⁿ x.