Spectral residuals: hub_spec, hlb_spec, and the per-stratum lower bound #
This module discharges three residuals of the MET final composer
Oseledets.oseledets_filtration_of_upper:
lyapunovSpectrum_subset_distinctExp_of_slowflag— every realized exponent is one of the deterministiclam0 i;distinctExp_subset_lyapunovSpectrum_of_slowflag— every deterministic exponent is realized;specList_le_liminf_inv_mul_log_norm_cocycle_apply_of_slowflag— the per-stratum liminf lower bound.
All three are derived from two hypotheses with fixed shapes: hident (band-projector
convergence to the indicator CFC of lambdaHat) and hslowflag
(vslow (exp t) = lambdaSublevel t).
Spectral foundation: eigenvalues of lambdaHat are exp (lamSing i) #
The spectrum of the sanitized limit is {exp (lamSing i)}. A.e., the Oseledets limit is
Hermitian, so lambdaHat A T x = oseledetsLimit A T x; the ℝ-spectrum of a Hermitian matrix is
the range of its eigenvalues (spectrum_real_eq_range_eigenvalues), the (unsorted) eigenvalue range
equals the sorted-eigenvalue range, and the sorted eigenvalues are exp (lamSing i)
(oseledetsLimit_eigenvalues₀_eq).
Local constancy of the slow projector across an eigenvalue-free gap #
slowProjector is constant across a gap with no eigenvalue. If the spectrum of
lambdaHat A T x is {exp (lamSing j)} and no lamSing j lies in the half-open interval
(t₁, t₂] (i.e. each is ≤ t₁ or > t₂), then the two indicator cutoffs Iic (exp t₁)
and Iic (exp t₂) agree on the spectrum, so the corresponding slow projectors coincide.
vslow inherits local constancy from slowProjector.
Nested slow projectors and the difference (band) projector #
Nested slow projectors multiply to the smaller. For t₁ ≤ t₂,
slowProjector (exp t₁) · slowProjector (exp t₂) = slowProjector (exp t₁), since the smaller
sublevel indicator absorbs the larger on the spectrum.
A CFC is nonzero if its symbol is nonzero at some eigenvalue. If g is continuous on the
spectrum of lambdaHat A T x and g (exp (lamSing j)) ≠ 0, then cfc g (lambdaHat A T x) ≠ 0
(via eqOn_of_cfc_eq_cfc against cfc 0).
The slow projector at exp s is nonzero when s is realized by some eigenvalue lamSing j:
cfc (indicator (Iic (exp s))) lambdaHat takes value 1 at the eigenvalue
exp (lamSing j) ≤ exp s, so it is not the zero CFC.
Range membership for idempotent matrices #
toEuclideanLin turns matrix multiplication into composition (applied form).
a.e. identification lamSing = lam0 #
A.e., the per-point exponents lamSing A T x j equal the deterministic lam0 j for every
j : Fin d.
Upper spectral bound: hub_spec #
hub_spec: every realized exponent is deterministic. A.e., the limsup spectrum is
contained in the deterministic distinct-exponent set distinctExp lam0 d.
Lower spectral bound: hlb_spec #
hlb_spec: every deterministic exponent is realized. A.e., the deterministic
distinct-exponent set is contained in the limsup spectrum: each lam0 j (j < d) is the value
lambdaBar A T x v of some nonzero v, exhibited by the rank-jump of the slow projector at the
eigenvalue exp (lamSing j) = exp (lam0 j).
Per-stratum liminf lower bound #
Per-stratum liminf lower bound (hlb). On each stratum vflag i.castSucc \ vflag i.succ,
the cocycle grows at least at rate specList A T x i. The argument sweeps thresholds
c = exp (specList i − ε') strictly below the stratum eigenvalue up to it: for each such c
(not an eigenvalue), 1 - slowProjector c = cfc (indicator (Ioi c)) lambdaHat has nonzero
action on v (else v ∈ vslow c, contradicting lambdaBar v = specList i > log c), and
hident supplies the band-projector convergence feeding log_le_liminf_log_cocycle_apply.