Margulis–Ruelle inequality

margulis_ruelle

Submitter: Kim Morrison.

Notes: Margulis (1968) / Ruelle (1978): for a C²-diffeomorphism T of a compact surface and a T-invariant ergodic probability measure μ, the Kolmogorov–Sinai entropy is bounded by the sum of the positive parts of the Lyapunov exponents, h_μ(T) ≤ λ₁⁺ + λ₂⁺. Shares the §103 trusted helpers (kolmogorovSinaiEntropy, lyapunov* via totalized sSup/limsup; genuine in the compact-C² regime). Not in Mathlib (no KS entropy, no Lyapunov exponents). Candidate from §103 of the Knill survey.

Source: D. Ruelle, *An inequality for the entropy of differentiable maps*, Bol. Soc. Brasil. Mat. 9 (1978); G. A. Margulis (1968, unpublished). Knill, *Some fundamental theorems in mathematics*, §103.

Informal solution: Ruelle's inequality. Cover the manifold by a fine partition and estimate the number of partition atoms an orbit can be distinguished into after n steps: the differential DT^n expands volumes by at most ∏ⱼ exp(n·λⱼ⁺) up to subexponential factors, so the n-step refinement ∨_{k<n} T^{-k}P has at most exp(n·∑λⱼ⁺ + o(n)) essential atoms. Hence (1/n)H_μ(∨ T^{-k}P) ≤ ∑λⱼ⁺ + o(1), and taking the partition-supremum gives h_μ ≤ ∑λⱼ⁺. Uses Oseledec exponents and the volume-growth bound; not in Mathlib.

theorem declaration uses `sorry`margulis_ruelle (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
      ≤ max 0 (∫ x, lyapunovUpperAt T x ∂μ)
          + max 0 (∫ x, lyapunovLowerAt T x ∂μ) := 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 ≤
  max 0 (∫ (x : EucPlane), lyapunovUpperAt T x ∂μ) + max 0 (∫ (x : EucPlane), lyapunovLowerAt T x ∂μ)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.