Spectrum constancy: identifying the per-point spectrum with the deterministic exponent set

Oseledets.specList_eq_expEnum_of_lyapunovSpectrum_const (in FiltrationInterfaceReduction.lean) reduces the hspec interface of the final assembly to the single hypothesis

hspecconst : ∀ᵐ x ∂μ, lyapunovSpectrum A T x = distinctExp lam0 d.

This file discharges hspecconst. The per-point limsup spectrum lyapunovSpectrum A T x is the finite set of values of the upper Lyapunov growth function lambdaBar A T x on nonzero vectors (Oseledets.lyapunovSpectrum, Oseledets.mem_lyapunovSpectrum). Pinning that finite set to the deterministic distinct-exponent set distinctExp lam0 d is a Finset.Subset.antisymm of two per-vector inclusions:

• upper inclusion lyapunovSpectrum A T x ⊆ distinctExp lam0 d — every realized lambdaBar value is one of the deterministic singular-value exponents lam0 i (i < d). This is the growth→exponent direction; its per-vector core is the spectral upper bound, the genuine analytic step of the multiplicative ergodic theorem (via the determinant/tempering squeeze).

• lower inclusion distinctExp lam0 d ⊆ lyapunovSpectrum A T x — every distinct deterministic exponent lam0 i is attained by some nonzero vector, i.e. lies in the lambdaBar-range. Its per-vector core is the lower bound (log_le_liminf_log_cocycle_apply) combined with the stratum-exact lambdaBar_eq_on_stratum.

The two inclusions compose to the constant distinctExp lam0 d, so ergodic constancy of the spectrum is automatic — the limit set is deterministic by construction, hence trivially T-invariant and constant; no separate Finset ℝ measurability / ergodic-averaging step is needed once the identification is in hand. For completeness we also record, unconditionally from lyapunovSpectrum_equivariant_ae together with ergodicity, that the identification self-propagates: if it holds it holds at T x too, and on the full orbit.

What is unconditional vs. hypothesis-gated

• lyapunovSpectrum_eq_of_subsets and lyapunovSpectrum_eq_distinctExp_of_subsets_ae are unconditional Finset algebra: they turn the two per-vector inclusions into the Finset identity / the hspec interface, using nothing but Oseledets.specList_eq_expEnum_of_lyapunovSpectrum_const.
• lyapunovSpectrum_const_invariant_ae is unconditional (from lyapunovSpectrum_equivariant_ae): the identification, once true a.e., is T-invariant a.e.
• The two per-vector inclusion hypotheses hub_spec / hlb_spec are the analytic interface. The lower one follows from the established lower bound; the upper one is the spectral upper bound. They are stated here in a minimal cleanly-typed Finset shape so that the surrounding assembly can plug the per-vector outputs in directly.

Unconditional Finset algebra: two inclusions ⟹ the identity

theorem Oseledets.lyapunovSpectrum_eq_of_subsets {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} {x : X} {lam0 : ℕ → ℝ} (hub : lyapunovSpectrum A T x ⊆ distinctExp lam0 d) (hlb : distinctExp lam0 d ⊆ lyapunovSpectrum A T x) : lyapunovSpectrum A T x = distinctExp lam0 d

The spectrum identity from the two per-vector inclusions (pointwise). If, at the point x, every spectrum value is a deterministic exponent and every deterministic exponent is attained, then the per-point limsup spectrum equals the deterministic distinct-exponent set.

theorem Oseledets.lyapunovSpectrum_eq_distinctExp_of_subsets_ae {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (lam0 : ℕ → ℝ) (hub_spec : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x ⊆ distinctExp lam0 d) (hlb_spec : ∀ᵐ (x : X) ∂μ, distinctExp lam0 d ⊆ lyapunovSpectrum A T x) : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x = distinctExp lam0 d

hspecconst from the two a.e. per-vector inclusions. The minimal cleanly-typed reduction: the a.e. upper inclusion (spectrum ⊆ distinctExp, the spectral upper bound) and the a.e. lower inclusion (distinctExp ⊆ spectrum, the attainment/lower-bound layer) give the a.e. spectrum constancy lyapunovSpectrum A T x = distinctExp lam0 d consumed by specList_eq_expEnum_of_lyapunovSpectrum_const.

theorem Oseledets.specList_eq_expEnum_of_subsets_ae {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} {T : X → X} (A : X → Matrix (Fin d) (Fin d) ℝ) (lam0 : ℕ → ℝ) (hub_spec : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x ⊆ distinctExp lam0 d) (hlb_spec : ∀ᵐ (x : X) ∂μ, distinctExp lam0 d ⊆ lyapunovSpectrum A T x) : ∀ᵐ (x : X) ∂μ, ∃ (h : specCard A T x = numExp lam0 d), ∀ (i : Fin (specCard A T x)), specList A T x i = expEnum lam0 d (Fin.cast h i)

The hspec interface, discharged from the two a.e. per-vector inclusions. Composes lyapunovSpectrum_eq_distinctExp_of_subsets_ae with specList_eq_expEnum_of_lyapunovSpectrum_const: the output is exactly the hspec hypothesis of oseledets_filtration_of_interfaces.

Reducing the inclusions to the native lambdaBar shape

The two Finset inclusions are equivalent, on the a.e. good set where lambdaBar A T x is an IsUltrametricGrowth function (isUltrametricGrowth_lambdaBar), to per-vector lambdaBar statements:

• upper inclusion ⟺ every realized value lambdaBar A T x v (v ≠ 0) is some lam0 j (j < d) — this is the spectral-upper-bound output (lambdaBar v = λᵢ on each stratum, the values being the deterministic exponents);
• lower inclusion ⟺ every lam0 j (j < d) is realized by some nonzero v — the attainment/ lower-bound layer.

These reductions are unconditional mem_lyapunovSpectrum/mem_distinctExp unfoldings; they let the per-vector outputs be fed in without first repackaging into Finsets.

theorem Oseledets.lyapunovSpectrum_subset_iff_lambdaBar_mem {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} {x : X} {lam0 : ℕ → ℝ} (hx : IsUltrametricGrowth (lambdaBar A T x)) : lyapunovSpectrum A T x ⊆ distinctExp lam0 d ↔ ∀ (v : EuclideanSpace ℝ (Fin d)), v ≠ 0 → ∃ j < d, lam0 j = lambdaBar A T x v

Upper inclusion in native lambdaBar/lam0 form. On the IsUltrametricGrowth good set, the Finset upper inclusion spectrum ⊆ distinctExp is exactly: every value of lambdaBar A T x on a nonzero vector is one of the deterministic exponents lam0 j (j < d).

theorem Oseledets.distinctExp_subset_iff_lambdaBar_attained {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} {x : X} {lam0 : ℕ → ℝ} (hx : IsUltrametricGrowth (lambdaBar A T x)) : distinctExp lam0 d ⊆ lyapunovSpectrum A T x ↔ ∀ j < d, ∃ (v : EuclideanSpace ℝ (Fin d)), v ≠ 0 ∧ lambdaBar A T x v = lam0 j

Lower inclusion in native lam0/lambdaBar form. On the IsUltrametricGrowth good set, the Finset lower inclusion distinctExp ⊆ spectrum is exactly: every deterministic exponent lam0 j (j < d) is realized as lambdaBar A T x v for some nonzero v.

theorem Oseledets.lyapunovSpectrum_eq_distinctExp_of_lambdaBar {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (lam0 : ℕ → ℝ) (hub_lam : ∀ᵐ (x : X) ∂μ, ∀ (v : EuclideanSpace ℝ (Fin d)), v ≠ 0 → ∃ j < d, lam0 j = lambdaBar A T x v) (hlb_lam : ∀ᵐ (x : X) ∂μ, ∀ j < d, ∃ (v : EuclideanSpace ℝ (Fin d)), v ≠ 0 ∧ lambdaBar A T x v = lam0 j) : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x = distinctExp lam0 d

hspecconst from the native per-vector outputs. Combines the two lambdaBar-level reductions with the a.e. IsUltrametricGrowth good set: given a.e. that every realized lambdaBar value is a deterministic exponent (hub_lam, the spectral upper bound) and every deterministic exponent is attained (hlb_lam, the lower-bound/attainment layer), the spectrum is a.e. the deterministic constant distinctExp lam0 d.

Ergodic constancy of the spectrum

The deterministic target distinctExp lam0 d is constant in x, so the identification lyapunovSpectrum A T x = distinctExp lam0 d is automatically T-invariant. We make the self-propagation explicit and unconditional from lyapunovSpectrum_equivariant_ae: where the spectrum equals the deterministic constant and is A-equivariant, the same holds at T x. This is the precise ergodic-constancy content — once the (deterministic) value is identified, ergodicity adds nothing further, because a deterministic function is already constant.

theorem Oseledets.lyapunovSpectrum_const_invariant_ae {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (lam0 : ℕ → ℝ) (hconst : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x = distinctExp lam0 d) : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x = distinctExp lam0 d ∧ lyapunovSpectrum A T (T x) = distinctExp lam0 d

Self-propagation of the spectrum identity along T (a.e.). Unconditional from lyapunovSpectrum_equivariant_ae: if a.e. lyapunovSpectrum A T x = distinctExp lam0 d, then a.e. lyapunovSpectrum A T (T x) = distinctExp lam0 d as well. Together with the a.e. equivariance lyapunovSpectrum A T x = lyapunovSpectrum A T (T x) this exhibits the identification as T-invariant, i.e. the spectrum is a.e. equal to the same deterministic constant set at x and at T x.

End-to-end: the hspec interface under the standing hypotheses

Bundling everything: under the standard standing hypotheses, given the two analytic per-vector inclusions, the hspec interface (and hence — via the FiltrationInterfaceReduction results — the oseledets_filtration hspec slot) is discharged. The signature lists the full standing hypotheses so it slots directly into the surrounding assembly, even though the proof only needs the two inclusions; this fixes the shape the spectral upper bound must provide.

theorem Oseledets.specList_eq_expEnum_of_subsets_standing {X : Type u_1} [MeasurableSpace X] {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (hT : Ergodic T μ) (A : X → Matrix (Fin d) (Fin d) ℝ) (hA : ∀ (x : X), (A x).det ≠ 0) (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (lam0 : ℕ → ℝ) (hub_spec : ∀ᵐ (x : X) ∂μ, lyapunovSpectrum A T x ⊆ distinctExp lam0 d) (hlb_spec : ∀ᵐ (x : X) ∂μ, distinctExp lam0 d ⊆ lyapunovSpectrum A T x) : ∀ᵐ (x : X) ∂μ, ∃ (h : specCard A T x = numExp lam0 d), ∀ (i : Fin (specCard A T x)), specList A T x i = expEnum lam0 d (Fin.cast h i)

Standing-hypotheses wrapper for the hspec interface. Under Ergodic T μ, a probability measure, measurable invertible log-integrable A (and A⁻¹), and the two per-vector spectrum inclusions, the hspec hypothesis of oseledets_filtration_of_interfaces holds.