DiagonalEntropy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Entropy symmetry for the actual diagonal action

The time-reversal theorem applies to right translations by diagonal matrices. The final lemma combines it with the precise positive-root entropy formula of EKL (2006), Proposition 3.1(3). That formula remains an explicit hypothesis here; time reversal and the coefficient balance are proved.

theorem OAI.DukePrimeDegree.diagonal_entropy_neg line 25

Source documentation

Time reversal for the diagonal action on the arithmetic quotient.

theorem diagonal_entropy_neg (d : ℕ)
    (ell : Fin (d + 1) → ℝ) (hell : ∑ i, ell i = 0)
    (μ : Measure (X (d + 1)))
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ) (t : ℝ) :
    measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell (-t))) =
      measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell t)) := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow

lemma OAI.DukePrimeDegree.diagonalOneParameter_neg_weights line 43
lemma OAI.DukePrimeDegree.rootEntropyForm_nonneg line 56

theorem OAI.DukePrimeDegree.balanced_of_diagonal_entropy_formula line 65

Source documentation

The exact entropy-formula input suffices to balance the coefficients; no separate balance or time-reversal assumption is needed.

theorem balanced_of_diagonal_entropy_formula
    (d : ℕ) (μ : Measure (X (d + 1)))
    (hA : ∀ u : LogCoordinates d,
      μ.map (fun x => rightAction x (diagonalFlow u)) = μ)
    (w : Fin (d + 1) → Fin (d + 1) → ℝ) (hw : ∀ i j, 0 ≤ w i j)
    (hformula : ∀ (ell : Fin (d + 1) → ℝ) (hell : ∑ i, ell i = 0),
      measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell 1)) =
        ENNReal.ofReal (rootEntropyForm w ell)) :
    ∀ i, ∑ j, w i j = ∑ j, w j i := by
…

Mentions: OAI.DukePrimeDegree.diagonalFlow, OAI.DukePrimeDegree.rootEntropyForm