The transversality crux of the two-sided Oseledets theorem #
This module establishes the transversality crux χ⁺ + χ⁻ ≥ 0: if a
nonzero vector has forward (restricted) growth rate ≤ a along the backward orbit and backward
decay rate ≤ b with a + b < 0, then it cannot exist. Concretely the opposite-sign
sublevels of the forward and backward Oseledets filtrations are transverse, and the resulting
dimension count is the combinatorial input consumed by reflect_of_counting_and_sum.
The architecture:
inf_eq_bot_of_neg_sum— the per-point crux. For a forward level familyVfamwhose backward-orbit envelope has limsup≤ aand a backward levelUxalong which a nonzero vector decays with limsup≤ b, ifa + b < 0thenVfam x ⊓ Ux = ⊥. The argument writesv = A⁽ⁿ⁾(Sⁿx) · (B⁽ⁿ⁾(x) v)via the cocycle identitycocycle_succ', uses forward equivariance to placeB⁽ⁿ⁾(x) v ∈ Vfam(Sⁿx), and boundslog‖v‖ ≤ log‖A⁽ⁿ⁾(Sⁿx)·P‖ + log‖B⁽ⁿ⁾(x) v‖, whose normalized limit is≤ a + b < 0, forcing‖v‖ = 0.ae_crux— assembles the per-point crux a.e., for all forward level / backward level pairs(i, s)withλᵢ + μₛ < 0:V i.castSucc x ⊓ W s.castSucc x = ⊥. The envelope comes fromae_limsup_restricted_backward_le, the backward decay from the backward strong export (oseledets_filtration_dimsapplied to(T.symm, backwardGen A T)), and all the a.e. facts are bundled onto a single biinvariant conull good set (exists_conull_biinvariant); the level quantifiers range over finiteFin k × Fin l.ae_counting— the counting bound, holding a.e. and hence (being a deterministic inequality on the spectra) outright:∀ a b, a + b < 0 → #{j<d | lam0 j ≤ a} + #{j<d | mu0 j ≤ b} ≤ d. Thresholds are converted to levels via the largest enumerated exponent≤ a(resp.≤ b), the dimension formulaoseledets_filtration_dimsidentifies the filtration finranks with the counts, and the Grassmann identitySubmodule.finrank_sup_add_finrank_inf_eqwithV ⊓ W = ⊥fromae_cruxcloses the count.
The per-point transversality crux #
The per-point transversality crux.
Let A be an everywhere-invertible generator over the invertible system T : X ≃ᵐ X, with
backward generator B = backwardGen A T running over S = T.symm. Suppose:
henv: the backward-orbit envelope of a forward level familyVfamat the pointxhas limsup at mosta, i.e.limsup (1/n) log ‖A⁽ⁿ⁾(Sⁿx) · P_{Vfam(Sⁿx)}‖ ≤ a(with the sequence bounded above,henvbdd);hmem: forward equivariance places the backward image of any intersection vector into the forward level along the backward orbit,B⁽ⁿ⁾(x) v ∈ Vfam(Sⁿx);hdec: every nonzero intersection vector decays backward with limsup at mostb(bounded above,hdecbdd);hsum:a + b < 0.
Then Vfam x ⊓ Ux = ⊥. Indeed for a nonzero v in the intersection,
v = A⁽ⁿ⁾(Sⁿx) · (B⁽ⁿ⁾(x) v) (the cocycle identity cocycle_succ'), so
log‖v‖ ≤ log ‖A⁽ⁿ⁾(Sⁿx) · P‖ + log ‖B⁽ⁿ⁾(x) v‖; dividing by n and letting n → ∞ the right
side has limsup ≤ a + b < 0 while the left side tends to 0, a contradiction.
The a.e. crux and the counting bound #
Membership equivariance along the backward orbit, derived from forward equivariance.
If B⁽ᵏ⁾(x) v ∈ Vfam(Sᵏx) is to be shown for all k, it suffices to know one-step
equivariance of A/Vfam along the backward orbit (the projection-conjugation form) together
with v ∈ Vfam x.
The backward-orbit envelope converges (a.e.). For the forward Oseledets level
Vᵢ = V i.castSucc, the floor-absorbed restricted operator norm along the backward orbit
converges to the Lyapunov exponent λᵢ:
(1/n) log ‖A⁽ⁿ⁾(Sⁿx) · P_{Vᵢ(Sⁿx)}‖ → λᵢ a.e.
This is the convergent strengthening of ae_limsup_restricted_backward_le (whose
limsup ≤ λᵢ is the consumed direction): it is obtained from the backward Kingman limit
restLog_backward_kingman (shared constant c), the identification c = λᵢ
(restricted_const_eq), and the floor absorption along the backward orbit
(restLog_eq_on_good). The convergence supplies the IsBoundedUnder proviso that the crux
needs, while the rate bound itself is taken from ae_limsup_restricted_backward_le.
The a.e. transversality crux.
For the forward Oseledets filtration V (with exponents expEnum lam0 d) of the system
(T, A) and the backward Oseledets filtration W (with exponents expEnum mu0 d) of the
backward system (T.symm, backwardGen A T), at a.e. x the opposite-sign interior sublevels
are transverse: for every forward level i and backward level s with
λᵢ + μₛ < 0, V i.castSucc x ⊓ W s.castSucc x = ⊥.
The proof bundles, on a single conull set, the backward-orbit envelope
(ae_limsup_restricted_backward_le, with the IsBoundedUnder proviso from the convergent
strengthening ae_tendsto_restricted_backward), the forward equivariance along the backward
orbit (ae_forall_iterate_of_ae over T.symm + mem_iterate_backward_of_orbit), and the
backward growth limits (the backward strong-export growth clause + flag descent
exists_stratum), then applies the per-point crux inf_eq_bot_of_neg_sum. All quantifiers
over levels range over the finite types Fin (numExp lam0 d) and Fin (numExp mu0 d).
Threshold-to-level conversion and the counting bound #
Threshold-to-level conversion. If the sublevel count #{j < d | p j ≤ a} of an
enumeration p is positive, then there is a distinct-exponent level i whose value is ≤ a
and whose sublevel count agrees with the count at a (no realized p-value lies strictly
between expEnum p d i and a).
The counting bound. At a.e. x — hence (being a deterministic inequality on the
spectra) outright — for all thresholds a, b with a + b < 0,
#{j < d | lam0 j ≤ a} + #{j < d | mu0 j ≤ b} ≤ d.
The bound is the combinatorial input consumed by reflect_of_counting_and_sum.
Each positive count is realized by a forward (resp. backward) interior level via
exists_level_eq_countLe, the dimension formula oseledets_filtration_dims identifies the
filtration finrank with the count, and the Grassmann identity
Submodule.finrank_sup_add_finrank_inf_eq with the crux
V i.castSucc x ⊓ W s.castSucc x = ⊥ (from ae_crux) bounds the sum by
finrank (V ⊔ W) ≤ d.