Top singular value = operator norm, and the k = 1 singular exponent tie-in

This module supplies the infrastructure lemma left open by Oseledets/Lyapunov/Extensions/SingularExponentBounds.lean: the largest singular value of a matrix equals its L2 operator norm,

σ₀(toEuclideanLin M) = ‖M‖.

The singular values LinearMap.singularValues are the descending square roots of the eigenvalues of adjoint f ∘ₗ f, so σ₀ is the largest one. The bound σ₀ ≤ ‖M‖ is already available (Oseledets.sigma_le_opNorm). The reverse ‖M‖ ≤ σ₀ is the new content: for every vector x, ‖f x‖² = ⟪(adjoint f ∘ₗ f) x, x⟫ = Σᵢ eᵢ ⟪uᵢ, x⟫² ≤ e₀ Σᵢ ⟪uᵢ, x⟫² = σ₀² ‖x‖², where u is the eigenvector basis of adjoint f ∘ₗ f and e its descending eigenvalues (e₀ = σ₀²). Hence ‖f x‖ ≤ σ₀ ‖x‖, giving ‖M‖ = ‖toEuclideanLin M‖ ≤ σ₀ via ContinuousLinearMap.opNorm_le_bound.

With σ₀ = ‖M‖ in hand, the k = 1 singular-value product collapses to the operator norm (sprod A T 1 n x = ‖A⁽ⁿ⁾(x)‖), so the cumulative forward singular exponent γ₁ is exactly the forward log⁺-operator-norm limsup (forwardPosLogNormLimsup); this is the identity that SingularExponentBounds.lean could only state as a one-sided ceiling. Under ergodicity it pins γ₁ to the a.e.-constant forward top value λ₁⁺.

Main results

• Oseledets.top_singularValue_eq_opNorm — σ₀(toEuclideanLin M) = ‖M‖ (the crux infra lemma).
• Oseledets.sprod_one_eq_opNorm — sprod A T 1 n x = ‖A⁽ⁿ⁾(x)‖.
• Oseledets.forwardSingularExponent_one_eq — γ₁(x) = forwardPosLogNormLimsup A T x (deterministic, every x).
• Oseledets.ae_forwardSingularExponent_one_eq_topExponent — under ergodicity, γ₁ = (λ₁⁺ : EReal) μ-a.e. for a real constant λ₁⁺ (the headline tie-in).

References

• M. Viana, Lectures on Lyapunov Exponents, Cambridge Studies in Adv. Math. 145 (2014).

theorem LinearMap.norm_apply_le_top_singularValue {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (f : E →ₗ[ℝ] F) [Nonempty (Fin (Module.finrank ℝ E))] (x : E) : ‖f x‖ ≤ f.singularValues 0 * ‖x‖

Top singular value bounds the image norm. For every x, ‖f x‖ ≤ σ₀(f) · ‖x‖. Expanding x in the eigenvector basis u of adjoint f ∘ₗ f (with descending eigenvalues e, so e₀ = σ₀² is the largest), ‖f x‖² = ⟪(adjoint f ∘ₗ f) x, x⟫ = Σᵢ eᵢ ⟪uᵢ, x⟫² ≤ e₀ Σᵢ ⟪uᵢ, x⟫² = σ₀² ‖x‖².

theorem Oseledets.top_singularValue_eq_opNorm {d : ℕ} [NeZero d] (M : Matrix (Fin d) (Fin d) ℝ) : (Matrix.toEuclideanLin M).singularValues 0 = ‖M‖

Top singular value = L2 operator norm. For a square matrix M : Matrix (Fin d) (Fin d) ℝ with d ≠ 0, the largest singular value of toEuclideanLin M equals the L2 operator norm ‖M‖: σ₀(toEuclideanLin M) = ‖M‖. The ≤ direction is Oseledets.sigma_le_opNorm; the ≥ direction is ContinuousLinearMap.opNorm_le_bound fed the per-vector bound LinearMap.norm_apply_le_top_singularValue (‖f x‖ ≤ σ₀ · ‖x‖), using ‖M‖ = ‖LinearMap.toContinuousLinearMap (toEuclideanLin M)‖.

theorem Oseledets.sprod_one_eq_opNorm {X : Type u_1} {T : X → X} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (n : ℕ) (x : X) : sprod A T 1 n x = ‖cocycle A T n x‖

sprod at k = 1 is the operator norm. The top-1 singular-value product is just the largest singular value (Finset.prod_range_one), which equals ‖A⁽ⁿ⁾(x)‖ (top_singularValue_eq_opNorm): sprod A T 1 n x = ‖cocycle A T n x‖.

theorem Oseledets.forwardSingularExponent_one_eq {X : Type u_1} {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (x : X) : forwardSingularExponent A T 1 x = forwardPosLogNormLimsup A T x

γ₁ is exactly the forward log⁺-operator-norm limsup (deterministic, every x). Rewriting the defining limsup of γ₁ through sprod_one_eq_opNorm (sprod_1 = ‖A⁽ⁿ⁾‖) turns it into the limsup of (1/n) log⁺‖A⁽ⁿ⁾‖, i.e. forwardPosLogNormLimsup A T x. This sharpens the one-sided ceiling forwardSingularExponent_le_natCast_mul (at k = 1) to an equality.

theorem Oseledets.ae_forwardSingularExponent_one_eq_topExponent {X : Type u_1} [MeasurableSpace X] {T : X → X} {d : ℕ} {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] [NeZero d] (hT : Ergodic T μ) {A : X → Matrix (Fin d) (Fin d) ℝ} (hAmeas : Measurable A) (hint : IntegrableLogNorm A μ) : ∃ (lam : ℝ), ∀ᵐ (x : X) ∂μ, forwardSingularExponent A T 1 x = ↑lam

The k = 1 singular exponent tie-in (headline). For an ergodic measure-preserving T and a possibly-singular measurable generator with log⁺‖A‖ ∈ L¹, there is a real constant λ₁⁺ (the forward top value of tendsto_top_posLogNorm) such that the cumulative forward singular exponent γ₁ equals (λ₁⁺ : EReal) for μ-a.e. x. Via forwardSingularExponent_one_eq, γ₁ is the limsup of the EReal-coerced (1/n) log⁺‖A⁽ⁿ⁾‖; on the a.e. convergence set this sequence tends to (λ₁⁺ : EReal) (continuous_coe_real_ereal), so its limsup is (λ₁⁺ : EReal) (Tendsto.limsup_eq).