Lai-Sang Young entropy–dimension–Lyapunov theorem

entropy_dimension_lyapunov

Submitter: Kim Morrison.

Notes: Lai-Sang Young (1982): for a C²-diffeomorphism T of a compact surface (modelled on EuclideanSpace ℝ (Fin 2) with a compact invariant K) and a T-invariant ergodic probability measure μ, h_μ(T) = dim(μ)·λ(T,μ)/2, where λ(T,μ) is the harmonic mean of (λ₁, −λ₂). Shares trusted (non-hole) helpers with the rest of §103: dimMeasure, kolmogorovSinaiEntropy (via sSup), entropyW/lyapunov* (via Filter.limsup), harmonicMeanLyapunov. These helpers are total functions (sSup/limsup are junk outside their intended bounded regime); in the compact-C² setting entropy and exponents are finite and the (DT^n)⁻¹ is genuine because T has a C² two-sided inverse. Mathlib has dimH, Ergodic, MeasurePreserving, Real.negMulLog, fderiv, but no Kolmogorov–Sinai entropy, no Lyapunov exponents/Oseledec, and none of these theorems. Candidate from §103 of the Knill survey.

Source: L.-S. Young, *Dimension, entropy and Lyapunov exponents*, Ergodic Theory Dynam. Systems 2 (1982), 109–124. Knill, *Some fundamental theorems in mathematics*, §103.

Informal solution: Young's argument relates the Kolmogorov–Sinai entropy, the Hausdorff dimension of μ, and the Lyapunov exponents for a surface diffeomorphism. Build a measurable partition into small dynamical rectangles aligned with the stable/unstable directions (Oseledec splitting); the entropy is computed along unstable manifolds (Shannon–McMillan–Breiman) while the pointwise dimension dim(μ) is governed by the contraction/expansion rates λ₁, −λ₂ via a Borel–Cantelli/covering argument. Equating the two expressions for the local scaling of μ-mass on dynamical balls gives h_μ = dim(μ)·(2λ₁(−λ₂)/(λ₁−λ₂))/2. Requires Oseledec MET, absolute continuity of the unstable foliation, and the entropy-via-increasing-partitions machinery, none in Mathlib.

theorem declaration uses `sorry`entropy_dimension_lyapunov (T T_inv : LeanEval.Dynamics.EucPlane → LeanEval.Dynamics.EucPlane)
    (hT_smooth : ContDiff ℝ 2 T)
    (hT_inv_smooth : ContDiff ℝ 2 T_inv)
    (hT_left : Function.LeftInverse T_inv T)
    (hT_right : Function.RightInverse T_inv T)
    (K : Set LeanEval.Dynamics.EucPlane)
    (hK_compact : IsCompact K)
    (hK_inv : T '' K = K)
    (μ : Measure LeanEval.Dynamics.EucPlane) [IsProbabilityMeasure μ]
    (hμ_supp : μ Kᶜ = 0)
    (hμ_pres : MeasurePreserving T μ μ)
    (hμ_erg : Ergodic T μ) :
    kolmogorovSinaiEntropy μ T =
      (dimMeasure μ).toReal *
        harmonicMeanLyapunov
          (∫ x, lyapunovUpperAt T x ∂μ)
          (∫ x, lyapunovLowerAt T x ∂μ) / 2 := byT:EucPlane → EucPlaneT_inv:EucPlane → EucPlanehT_smooth:ContDiff ℝ 2 ThT_inv_smooth:ContDiff ℝ 2 T_invhT_left:Function.LeftInverse T_inv ThT_right:Function.RightInverse T_inv TK:Set EucPlanehK_compact:IsCompact KhK_inv:T '' K = Kμ:Measure EucPlaneinst✝:IsProbabilityMeasure μhμ_supp:μ Kᶜ = 0hμ_pres:MeasurePreserving T μ μhμ_erg:Ergodic T μ⊢ kolmogorovSinaiEntropy μ T =
  (dimMeasure μ).toReal *
      harmonicMeanLyapunov (∫ (x : EucPlane), lyapunovUpperAt T x ∂μ) (∫ (x : EucPlane), lyapunovLowerAt T x ∂μ) /
    2
  sorryAll goals completed! 🐙

Solved by

Not yet solved.