The backward-orbit restricted envelope

For a fixed measurable family of subspaces V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d)) this module builds the restricted cocycle used in the transversality crux of the two-sided multiplicative ergodic theorem. The restricted generator is restGen A V x = A x * orthProjMatrix (V x) and the restricted log-norm cocycle is

restLog A V T n x = Real.log (‖cocycle (restGen A V) T n x‖ ⊔ sFloor A T n x)

where sFloor A T n x = ∏_{j<n} (‖(A (T^[j] x))⁻¹‖)⁻¹ is a strictly-positive floor.

The floor is the key device: plain log ‖cocycle (A·P)‖ fails to be subadditive at the "junk" points where the restricted product collapses to the zero matrix (log 0 = 0). The ⊔-floor makes the floored quantity everywhere strictly positive, so restLog is subadditive over T for all m, n, x — exactly the everywhere hypothesis Kingman's theorem needs. On a biinvariant conull good set (flag equivariance along the orbit plus V ≠ ⊥) the floor is absorbed and restLog n x = log ‖A⁽ⁿ⁾(x)·P_{V(x)}‖.

Main definitions

• Oseledets.restGen: the restricted generator x ↦ A x * orthProjMatrix (V x).
• Oseledets.sFloor: the strictly-positive floor ∏_{j<n} (‖(A (T^[j] x))⁻¹‖)⁻¹.
• Oseledets.restLog: the floored restricted log-norm cocycle.

Main results

• Oseledets.sFloor_pos, Oseledets.sFloor_mul: positivity and multiplicativity of the floor.
• Oseledets.isSubadditiveCocycle_restLog: restLog is an everywhere subadditive cocycle over T.
• Oseledets.measurable_restLog, Oseledets.integrable_restLog: measurability and integrability of each level.
• Oseledets.restLog_eq_on_good: on the good set the floor is absorbed, restLog n y = log ‖A⁽ⁿ⁾(y)·P_{V(y)}‖.
• Oseledets.restLog_kingman: Kingman over T for restLog with the constant identified as the limit of the integral means (via tendsto_kingman_ergodic_means).
• Oseledets.restLog_backward_kingman: the backward transfer — restLog ∘ (T.symm)^[·] is subadditive over T.symm with the same constant.

The restricted generator and the floor

noncomputable def Oseledets.restGen {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) : X → Matrix (Fin d) (Fin d) ℝ

The restricted generator x ↦ A x * orthProjMatrix (V x): the forward generator post-composed (on the right) with the orthogonal projection onto V x.

Equations

• Oseledets.restGen A V x = A x * Oseledets.orthProjMatrix (V x)

noncomputable def Oseledets.sFloor {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (n : ℕ) (x : X) : ℝ

The strictly-positive floor ∏_{j<n} (‖(A (T^[j] x))⁻¹‖)⁻¹. Multiplicative along the orbit; bounded below the cocycle norm on the good set.

Equations

• Oseledets.sFloor A T n x = ∏ j ∈ Finset.range n, ‖(A (T^[j] x))⁻¹‖⁻¹

noncomputable def Oseledets.restLog {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))) (T : X → X) (n : ℕ) (x : X) : ℝ

The floored restricted log-norm cocycle restLog A V T n x = log (‖cocycle (restGen A V) T n x‖ ⊔ sFloor A T n x).

Equations

• Oseledets.restLog A V T n x = Real.log (max ‖Oseledets.cocycle (Oseledets.restGen A V) T n x‖ (Oseledets.sFloor A T n x))

theorem Oseledets.max_mul_le_mul_max {a b c e : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (he : 0 ≤ e) : max (a * b) (c * e) ≤ max a c * max b e

For nonnegative reals, max (a*b) (c*d) ≤ max a c * max b d.

Positivity and multiplicativity of the floor

theorem Oseledets.sFloor_factor_pos {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (y : X) : 0 < ‖(A y)⁻¹‖⁻¹

Each floor factor (‖(A y)⁻¹‖)⁻¹ is strictly positive for an invertible generator.

theorem Oseledets.sFloor_pos {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : 0 < sFloor A T n x

The floor is strictly positive.

theorem Oseledets.sFloor_mul {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} (m n : ℕ) (x : X) : sFloor A T (m + n) x = sFloor A T m x * sFloor A T n (T^[m] x)

Floor multiplicativity. sFloor (m + n) x = sFloor m x * sFloor n (T^[m] x).

Everywhere subadditivity of the floored restricted log cocycle

theorem Oseledets.isSubadditiveCocycle_restLog {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] : IsSubadditiveCocycle T (restLog A V T)

Everywhere subadditivity. restLog A V T is a subadditive cocycle over T for all m, n, x (no a.e. caveat): the floor sFloor is strictly positive, so the ⊔ is always positive and Real.log is monotone with Real.log_mul available. This is precisely the everywhere hypothesis Kingman's theorem requires; plain log ‖cocycle (A·P)‖ fails to be subadditive at the junk points where the restricted product vanishes.

Elementary norm facts feeding the integrability sandwich

theorem Oseledets.norm_restGen_le {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (x : X) : ‖restGen A V x‖ ≤ ‖A x‖

‖restGen A V x‖ ≤ ‖A x‖: the projection is a contraction.

theorem Oseledets.norm_cocycle_restGen_le_prod {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} (n : ℕ) (x : X) : ‖cocycle (restGen A V) T n x‖ ≤ ∏ j ∈ Finset.range n, ‖A (T^[j] x)‖

‖cocycle (restGen A V) T n x‖ ≤ ∏_{j<n} ‖A (T^[j] x)‖.

theorem Oseledets.inv_norm_inv_le_norm {d : ℕ} {M : Matrix (Fin d) (Fin d) ℝ} [NeZero d] (hM : M.det ≠ 0) : ‖M⁻¹‖⁻¹ ≤ ‖M‖

(‖M⁻¹‖)⁻¹ ≤ ‖M‖ for an invertible matrix.

theorem Oseledets.posLog_eq_log_max_one {t : ℝ} (ht : 0 ≤ t) : t.posLog = Real.log (max t 1)

Real.posLog t = Real.log (t ⊔ 1) for t ≥ 0.

The sandwich bounds

theorem Oseledets.log_sFloor_le_restLog {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : Real.log (sFloor A T n x) ≤ restLog A V T n x

Lower sandwich. restLog n x ≥ log (sFloor n x) = -∑ log‖(A∘T^[j])⁻¹‖.

theorem Oseledets.log_sFloor_eq {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : Real.log (sFloor A T n x) = -birkhoffSum T (fun (y : X) => Real.log ‖(A y)⁻¹‖) n x

log (sFloor n x) = - birkhoffSum T (log‖A⁻¹‖) n x.

theorem Oseledets.restLog_le_birkhoffSum {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (n : ℕ) (x : X) : restLog A V T n x ≤ birkhoffSum T (fun (y : X) => ‖A y‖.posLog) n x

Upper sandwich. restLog n x ≤ birkhoffSum T (log⁺‖A‖) n x. The ⊔ is dominated by ∏ (‖A∘T^[j]‖ ⊔ 1), whose log is the positive-log Birkhoff sum.

Measurability and integrability of each level

theorem Oseledets.measurable_restGen {X : Type u_1} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hAmeas : Measurable A) (hV : MeasurableSubspace V) : Measurable (restGen A V)

The restricted generator is measurable when A and the subspace family are.

theorem Oseledets.measurable_sFloor {X : Type u_1} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} (hAmeas : Measurable A) (hTmeas : Measurable T) (n : ℕ) : Measurable fun (x : X) => sFloor A T n x

The floor is measurable.

theorem Oseledets.measurable_restLog {X : Type u_1} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} (hAmeas : Measurable A) (hV : MeasurableSubspace V) (hTmeas : Measurable T) (n : ℕ) : Measurable fun (x : X) => restLog A V T n x

Each level restLog n is measurable.

theorem Oseledets.integrable_restLog {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.IsFiniteMeasure μ] {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (hAmeas : Measurable A) (hV : MeasurableSubspace V) (hTmeas : Measurable T) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (n : ℕ) : MeasureTheory.Integrable (fun (x : X) => restLog A V T n x) μ

Integrability of each level. Each restLog n is integrable, via the sandwich -(birkhoffSum log⁺‖A‖ + birkhoffSum log⁺‖A⁻¹‖) ≤ restLog n ≤ birkhoffSum log⁺‖A‖ whose endpoints are integrable (mirroring integrable_logNorm_cocycle).

The good set: floor absorption and the unrestricted form

theorem Oseledets.orthProjMatrix_idem {d : ℕ} (K : Submodule ℝ (EuclideanSpace ℝ (Fin d))) : orthProjMatrix K * orthProjMatrix K = orthProjMatrix K

The orthogonal-projection matrix is idempotent.

theorem Oseledets.restEquivariant_iterate {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} {y : X} (hequiv : ∀ (k : ℕ), orthProjMatrix (V (T (T^[k] y))) * A (T^[k] y) * orthProjMatrix (V (T^[k] y)) = A (T^[k] y) * orthProjMatrix (V (T^[k] y))) (m : ℕ) : orthProjMatrix (V (T^[m] y)) * cocycle A T m y * orthProjMatrix (V y) = cocycle A T m y * orthProjMatrix (V y)

Multi-step flag equivariance. Given the one-step equivariance P(T z) · A z · P z = A z · P z along the orbit, the projection P(T^[m] y) fixes A⁽ᵐ⁾(y) · P y.

theorem Oseledets.cocycle_restGen_eq {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} {y : X} (hequiv : ∀ (k : ℕ), orthProjMatrix (V (T (T^[k] y))) * A (T^[k] y) * orthProjMatrix (V (T^[k] y)) = A (T^[k] y) * orthProjMatrix (V (T^[k] y))) (n : ℕ) : cocycle (restGen A V) T (n + 1) y = cocycle A T (n + 1) y * orthProjMatrix (V y)

The restricted matrix identity on the good set (levels ≥ 1). With the one-step flag equivariance along the orbit, cocycle (restGen A V) T (n+1) y = cocycle A T (n+1) y · P_{V y}. (At n = 0 the identity reads 1 = P_{V y}, which fails unless V y = ⊤; hence the n+1.)

theorem Oseledets.norm_inv_cocycle_le_prod {X : Type u_1} {d : ℕ} {A : X → Matrix (Fin d) (Fin d) ℝ} {T : X → X} (n : ℕ) (y : X) : ‖(cocycle A T n y)⁻¹‖ ≤ ∏ j ∈ Finset.range n, ‖(A (T^[j] y))⁻¹‖

‖(cocycle A T n y)⁻¹‖ ≤ ∏_{j<n} ‖(A (T^[j] y))⁻¹‖ (submultiplicativity of the inverse cocycle norm).

theorem Oseledets.sFloor_le_norm_cocycle_mul_proj {X : Type u_1} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] {y : X} (hVy : V y ≠ ⊥) (n : ℕ) : sFloor A T n y ≤ ‖cocycle A T n y * orthProjMatrix (V y)‖

Floor absorption. On the good set (V y ≠ ⊥), the floor is below the restricted cocycle norm: sFloor A T n y ≤ ‖cocycle A T n y · P_{V y}‖. (A unit vector v ∈ V y is fixed by the projection, so ‖A⁽ⁿ⁾ v‖ ≥ ‖(A⁽ⁿ⁾)⁻¹‖⁻¹ ≥ sFloor.)

theorem Oseledets.restLog_eq_on_good {X : Type u_1} {d : ℕ} [MeasurableSpace X] {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} {T : X → X} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] {y : X} (hequiv : ∀ (k : ℕ), orthProjMatrix (V (T (T^[k] y))) * A (T^[k] y) * orthProjMatrix (V (T^[k] y)) = A (T^[k] y) * orthProjMatrix (V (T^[k] y))) (hVy : V y ≠ ⊥) (n : ℕ) : restLog A V T (n + 1) y = Real.log ‖cocycle A T (n + 1) y * orthProjMatrix (V y)‖

The unrestricted form on the good set. With one-step flag equivariance along the orbit and V y ≠ ⊥, for n ≥ 1 the floor is absorbed and restLog A V T n y = log ‖A⁽ⁿ⁾(y) · P_{V y}‖. (This is the form consumed by the restricted exponent computation; the ⊔-floor was needed only for the everywhere-subadditivity feeding Kingman.)

Kingman over T and the means identification

theorem Oseledets.bddBelow_restLog_means {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.IsFiniteMeasure μ] {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (hAmeas : Measurable A) (hV : MeasurableSubspace V) (hTmeas : Measurable T) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : BddBelow (Set.range fun (n : ℕ) => (∫ (x : X), restLog A V T (n + 1) x ∂μ) / (↑n + 1))

The bounded-below proviso for restLog: each normalized integral mean is ≥ - ∫ log⁺‖A⁻¹‖. From the lower sandwich restLog n ≥ - birkhoffSum (log⁺‖A⁻¹‖) n.

theorem Oseledets.restLog_kingman {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X → X} (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (hAmeas : Measurable A) (hV : MeasurableSubspace V) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : ∃ (c : ℝ), Filter.Tendsto (fun (n : ℕ) => (∫ (x : X), restLog A V T (n + 1) x ∂μ) / (↑n + 1)) Filter.atTop (nhds c) ∧ ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * restLog A V T n x) Filter.atTop (nhds c)

Kingman over T with identified means. Under ergodicity, there is a constant χ_V that is both the limit of the integral means (∫ restLog (n+1)) / (n+1) and the μ-a.e. limit of (n : ℝ)⁻¹ • restLog n. The means identification (tendsto_kingman_ergodic_means) is what lets the backward transfer pin down the same constant.

Backward transfer: Kingman over T.symm with the same constant

theorem Oseledets.isSubadditiveCocycle_restLog_backward {X : Type u_1} {d : ℕ} [MeasurableSpace X] {T : X ≃ᵐ X} {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] : IsSubadditiveCocycle ⇑T.symm fun (n : ℕ) (x : X) => restLog A V (⇑T) n ((⇑T.symm)^[n] x)

The backward-shifted cocycle hₙ x = restLog A V T n (T.symm^[n] x) is subadditive over T.symm. The index juggle uses T^[n] ∘ T.symm^[m+n] = T.symm^[m] and the everywhere subadditivity of restLog.

theorem Oseledets.integral_restLog_backward {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X ≃ᵐ X} (hT : MeasureTheory.MeasurePreserving (⇑T) μ μ) [MeasureTheory.IsFiniteMeasure μ] {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (hAmeas : Measurable A) (hV : MeasurableSubspace V) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) (n : ℕ) : ∫ (x : X), restLog A V (⇑T) n ((⇑T.symm)^[n] x) ∂μ = ∫ (x : X), restLog A V (⇑T) n x ∂μ

The integral of the backward-shifted cocycle equals the integral of restLog: ∫ restLog n (T.symm^[n] x) ∂μ = ∫ restLog n x ∂μ (measure preservation of T.symm^[n]).

theorem Oseledets.restLog_backward_kingman {X : Type u_1} {d : ℕ} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] {T : X ≃ᵐ X} (hT : Ergodic (⇑T) μ) {A : X → Matrix (Fin d) (Fin d) ℝ} {V : X → Submodule ℝ (EuclideanSpace ℝ (Fin d))} (hA : ∀ (x : X), (A x).det ≠ 0) [NeZero d] (hAmeas : Measurable A) (hV : MeasurableSubspace V) (hint : IntegrableLogNorm A μ) (hint' : IntegrableLogNorm (fun (x : X) => (A x)⁻¹) μ) : ∃ (c : ℝ), Filter.Tendsto (fun (n : ℕ) => (∫ (x : X), restLog A V (⇑T) (n + 1) x ∂μ) / (↑n + 1)) Filter.atTop (nhds c) ∧ (∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * restLog A V (⇑T) n x) Filter.atTop (nhds c)) ∧ ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * restLog A V (⇑T) n ((⇑T.symm)^[n] x)) Filter.atTop (nhds c)

Backward transfer with the shared constant. There is a single constant χ_V such that the forward integral means converge to it, the forward normalized cocycle (1/n) restLog n converges to it μ-a.e. (over T), and the backward normalized cocycle (1/n) restLog n (T.symm^[n] x) converges to it μ-a.e. (over T.symm). The backward limit shares the forward constant precisely because the integral means of the two cocycles coincide (integral_restLog_backward) and Fekete limits are unique — this is where the means identification integral_restLog_backward is essential.