Exponent reflection for the two-sided Oseledets theorem #
This module establishes the exponent reflection principle: the backward singular spectrum is the reflected negation of the forward one.
The argument has two unconditional analytic inputs and one self-contained combinatorial core:
- Determinant identity (forward). For any deterministic exponent sequence
lam0realizing the a.e. per-index singular-value limits, the sum of the firstdvalues equals the integral oflog|det A|:∑_{j<d} lam0 j = ∫ x, log |(A x).det| ∂μ. This issum_lam0_eq_integral_log_abs_det, obtained fromOseledets.sumAllExp_eq_integral_log_abs_detofDetIdentity.leanby identifying the limit values via uniqueness of a.e. limits. - Determinant identity (backward). Applying the same to the backward system
(⇑T.symm, backwardGen A T)and changing variables (MeasurePreserving.integral_comp',Matrix.det_nonsing_inv,Real.log_inv) gives∑_{j<d} mu0 j = − ∑_{j<d} lam0 j(sum_mu0_eq_neg_sum_lam0). - Reflection combinatorics. A pure order/counting argument
(
reflect_of_counting_and_sum): two antitone tuplesp, q : ℕ → ℝon[0,d)with a counting bound (∀ a b, a + b < 0 → #{p ≤ a} + #{q ≤ b} ≤ d) and equal-opposite sums (∑ q = − ∑ p) satisfyq j = − p (d−1−j)pointwise. The counting bound is supplied byae_counting; here every reflection corollary takes it as a hypothesis, so this module does not depend onae_counting.
Main results #
Oseledets.sum_lam0_eq_integral_log_abs_det— forward determinant sum identity.Oseledets.sum_mu0_eq_neg_sum_lam0— backward sum is the negation of the forward sum.Oseledets.reflect_of_counting_and_sum— pure combinatorial reflection lemma.Oseledets.numExp_eq_of_counting,Oseledets.expEnum_eq_neg_rev_of_counting,Oseledets.backward_dim_count_of_counting— the reflection corollaries (number of distinct exponents, reflected-negated enumeration, backward dimension formula), each consuming the counting bound as a hypothesis.
The forward and backward determinant sum identities #
Forward determinant sum identity. Any deterministic exponent sequence lam0 that
realizes the a.e. per-index singular-value limits (e.g. the one produced by
exists_lam_tendsto_singularValue, exposed by oseledets_filtration_dims) satisfies
∑_{j<d} lam0 j = ∫ x, log |(A x).det| ∂μ.
Proof: the chosen spectrum exponents of Spectrum.lean realizes the same a.e. limits
(exponents_tendsto_log_singularValue); uniqueness of a.e. limits at a common conull
point forces lam0 j = exponents j for every j < d, so ∑_{j<d} lam0 j = sumAllExp,
which equals the integral by sumAllExp_eq_integral_log_abs_det.
The pointwise identity log |det (backwardGen A T x)| = − log |det (A (T.symm x))|,
from det (M⁻¹) = (det M)⁻¹ and log |r⁻¹| = − log |r|.
Backward determinant integral identity.
∫ x, log |det (backwardGen A T x)| ∂μ = − ∫ x, log |(A x).det| ∂μ, via the pointwise
inverse-determinant identity and the change of variables along the measure-preserving
T.symm.
Backward determinant sum identity. For any backward exponent sequence mu0
realizing the a.e. per-index singular-value limits of the backward cocycle
cocycle (backwardGen A T) (⇑T.symm), the sum of its first d values is the negation of
the forward sum:
∑_{j<d} mu0 j = − ∑_{j<d} lam0 j.
The pure combinatorial reflection lemma #
Reflection from counting bound and sum. Let p, q : ℕ → ℝ be antitone on [0, d).
If the counting bound ∀ a b, a + b < 0 → #{j < d | p j ≤ a} + #{j < d | q j ≤ b} ≤ d
holds and the sums are opposite, ∑_{j<d} q j = − ∑_{j<d} p j, then q is the reflected
negation of p: q j = − p (d − 1 − j) for every j < d.
Proof: the counting bound yields the pointwise lower bound q j ≥ − p (d − 1 − j)
(neg_p_rev_le_q); summing these and reindexing j ↦ d − 1 − j shows the sum of the
lower bounds equals − ∑ p = ∑ q, so the nonnegative slacks sum to zero, forcing equality
at every index (Finset.sum_eq_zero_iff_of_nonneg).
Reflection corollaries: distinct-exponent count, enumeration, dimension formula #
The backward distinct-exponent enumeration is the reflected negation of the forward
one. With q j = − p (d − 1 − j), the descending enumeration of q's distinct values at
index a equals the negation of the descending enumeration of p's distinct values at the
reversed index: expEnum q d a = − expEnum p d (a.rev'), where the index a.rev' lives in
Fin (numExp p d) after transporting along numExp q d = numExp p d.
Backward sublevel count = forward strict-superlevel count. With the reflection
q j = − p (d − 1 − j), for any threshold t the number of backward exponents at or below
−t equals the number of forward exponents at or above t, which is d minus the number
of forward exponents strictly below t:
#{j < d | q j ≤ −t} = d − #{j < d | p j < t}.
Backward dimension formula (robust strict-sublevel form). Specializing
backward_count_eq_of_counting at the forward Lyapunov exponent λᵢ = expEnum lam0 d i:
the backward interior dimension count at −λᵢ is d minus the number of forward
exponents strictly below λᵢ:
#{j < d | mu0 j ≤ −λᵢ} = d − #{j < d | lam0 j < λᵢ}.
This is the load-bearing reflection of the dimension counts. The blueprint's
λ_{i+1} form is obtained from this by forward_strict_count_eq_succ_of_counting, which
identifies #{lam0 j < λᵢ} with #{lam0 j ≤ λ_{i+1}} using the gap between consecutive
distinct exponents.
Consecutive-exponent gap. For consecutive distinct forward exponents
λᵢ = expEnum p d i and λ_{i+1} = expEnum p d i.succ, the forward exponents strictly
below λᵢ are exactly those at or below λ_{i+1} (no distinct value lies strictly between
two consecutive ones):
#{j < d | p j < λᵢ} = #{j < d | p j ≤ λ_{i+1}}.
Backward dimension formula (blueprint λ_{i+1} form). For consecutive forward
exponents, the backward interior dimension count at −λᵢ is d minus the number of
forward exponents at or below the next exponent λ_{i+1}:
#{j < d | mu0 j ≤ −λᵢ} = d − #{j < d | lam0 j ≤ λ_{i+1}}.