Pesin entropy formula (symplectic surface case)

pesin_formula

Submitter: Kim Morrison.

Notes: Pesin (1977), symplectic surface specialisation of Lai-Sang Young: for an ergodic surface diffeomorphism with dim(μ) = 2 and symmetric averaged exponents (∫λ₁ = −∫λ₂), h_μ(T) = ∫λ₁. The symplectic/volume-preserving case is encoded here via dimMeasure μ = 2 and the exponent-symmetry hypothesis (a consequence-form, not a full symplectic-derivative hypothesis package). Shares the §103 trusted helpers (totalized sSup/limsup; genuine in the compact-C² regime). Not in Mathlib (no KS entropy, no Lyapunov exponents, no Pesin formula). Candidate from §103 of the Knill survey.

Source: Ya. B. Pesin, *Characteristic Lyapunov exponents and smooth ergodic theory*, Russian Math. Surveys 32 (1977). Knill, *Some fundamental theorems in mathematics*, §103.

Informal solution: Pesin's formula h_μ = ∑ λⱼ⁺ for smooth invariant measures absolutely continuous w.r.t. volume. In the surface case with dim(μ) = 2 (full dimension forces μ ≪ volume) and λ₁ = −λ₂, the entropy equals the single positive exponent λ₁. Proof: the Margulis–Ruelle inequality gives h_μ ≤ λ₁⁺; the reverse inequality (the substantive half) uses absolute continuity of the unstable foliation / the SRB property to show entropy is at least the unstable expansion rate. Here it is obtained as the dim(μ)=2 specialisation of the Lai-Sang Young formula. Requires Pesin theory absent from Mathlib.

theorem declaration uses `sorry`pesin_formula (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 μ)
    (hμ_dim : dimMeasure μ = 2)
    (hlam_sym : ∫ x, lyapunovUpperAt T x ∂μ
        = -∫ x, lyapunovLowerAt T x ∂μ) :
    kolmogorovSinaiEntropy μ T = ∫ x, lyapunovUpperAt 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 μhμ_dim:dimMeasure μ = 2hlam_sym:∫ (x : EucPlane), lyapunovUpperAt T x ∂μ = -∫ (x : EucPlane), lyapunovLowerAt T x ∂μ⊢ kolmogorovSinaiEntropy μ T = ∫ (x : EucPlane), lyapunovUpperAt T x ∂μ
  sorryAll goals completed! 🐙

Solved by

Not yet solved.