Ultrametric growth functions

Pure finite-dimensional linear algebra underlying the Lyapunov→Oseledets arc: the ultrametric growth function abstraction that forces the Lyapunov spectrum to be finite (at most d = finrank ℝ E values) and its sublevel sets to be subspaces.

A real-valued function g on the nonzero vectors of a real vector space E is an ultrametric growth function (IsUltrametricGrowth) when it is scaling-invariant (g (c • v) = g v for c ≠ 0) and non-Archimedean (g (v + w) ≤ max (g v) (g w)). g 0 is never referenced; the v ≠ 0 side conditions are carried explicitly to avoid WithBot ℝ arithmetic.

The main results:

• IsUltrametricGrowth.add_eq_max_of_ne — the ultrametric inequality is an equality when the two values differ;
• IsUltrametricGrowth.linearIndependent_of_injOn — vectors with pairwise-distinct values are linearly independent;
• IsUltrametricGrowth.finite_range — the set of realized values is finite;
• IsUltrametricGrowth.sublevel — each sublevel set {v | v = 0 ∨ g v ≤ t} is a submodule;
• IsUltrametricGrowth.sublevel_mono — these sublevel submodules are monotone in t.

Reference: Oseledets multiplicative ergodic theorem, ultrametric growth function.

structure Oseledets.IsUltrametricGrowth {E : Type u_1} [AddCommGroup E] [Module ℝ E] (g : E → ℝ) : Prop

A real-valued function on the nonzero vectors of E is an ultrametric growth function if it is scaling-invariant and non-Archimedean. (g 0 is never referenced; v ≠ 0 side conditions are carried.)

• scaling (c : ℝ) (v : E) : c ≠ 0 → g (c • v) = g v

  g is invariant under nonzero scaling.

• ultra (v w : E) : v ≠ 0 → w ≠ 0 → v + w ≠ 0 → g (v + w) ≤ max (g v) (g w)

  g satisfies the strong (non-Archimedean) triangle inequality.

theorem Oseledets.IsUltrametricGrowth.neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → ℝ} (h : IsUltrametricGrowth g) (v : E) : g (-v) = g v

The value at -v equals the value at v (scaling by c = -1).

theorem Oseledets.IsUltrametricGrowth.add_eq_max_of_ne {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → ℝ} (h : IsUltrametricGrowth g) {v w : E} (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0) (hne : g v ≠ g w) : g (v + w) = max (g v) (g w)

Strict ultrametric: equality when the two values differ.

theorem Oseledets.IsUltrametricGrowth.sum_ne_zero_and_g_eq_sup' {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → ℝ} (h : IsUltrametricGrowth g) {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) {v : ι → E} (hv : ∀ i ∈ s, v i ≠ 0) (hinj : Set.InjOn (g ∘ v) ↑s) : ∑ i ∈ s, v i ≠ 0 ∧ g (∑ i ∈ s, v i) = s.sup' hs fun (i : ι) => g (v i)

A sum over a nonempty finset of nonzero vectors with pairwise-distinct g-values is nonzero, and its g-value equals the maximum of the individual g-values. This iterated add_eq_max_of_ne is the engine of ultrametric independence; the two conclusions are proved together because each induction step needs the tail subsum to be nonzero.

theorem Oseledets.IsUltrametricGrowth.linearIndependent_of_injOn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → ℝ} (h : IsUltrametricGrowth g) {ι : Type u_2} {v : ι → E} (hv : ∀ (i : ι), v i ≠ 0) (hinj : Function.Injective (g ∘ v)) : LinearIndependent ℝ v

Vectors of distinct values are linearly independent.

theorem Oseledets.IsUltrametricGrowth.finite_range {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → ℝ} [FiniteDimensional ℝ E] (h : IsUltrametricGrowth g) : (Set.range fun (v : { v : E // v ≠ 0 }) => g ↑v).Finite

The set of values is finite (the Lyapunov spectrum has at most d = finrank ℝ E elements).

def Oseledets.IsUltrametricGrowth.sublevel {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → ℝ} (h : IsUltrametricGrowth g) (t : ℝ) : Submodule ℝ E

The sublevel set {v | v = 0 ∨ g v ≤ t} is a submodule of E. Closure under addition is the non-Archimedean inequality, closure under scaling is scaling-invariance, and 0 lies in it via the left disjunct.

Equations

• h.sublevel t = { carrier := {v : E | v = 0 ∨ g v ≤ t}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem Oseledets.IsUltrametricGrowth.mem_sublevel {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → ℝ} (h : IsUltrametricGrowth g) (t : ℝ) (v : E) : v ∈ h.sublevel t ↔ v = 0 ∨ g v ≤ t

theorem Oseledets.IsUltrametricGrowth.sublevel_mono {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → ℝ} (h : IsUltrametricGrowth g) : Monotone h.sublevel

sublevel is monotone in the threshold t.