EntropyBalance.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Entropy symmetry and the root coefficient balance

The entropy formula in EKL (2006), Proposition 3.1, is a sum of positive root weights. Equality of the entropy of an invertible map and its inverse then gives the row/column balance. The finite algebraic implication uses trace-zero test weights independently of the dynamical entropy formula.

def OAI.DukePrimeDegree.rootEntropyForm line 22
Source documentation
The finite positive-root expression in the entropy formula.
```
def rootEntropyForm (w : ι → ι → ℝ) (t : ι → ℝ) : ℝ :=
…
```
lemma OAI.DukePrimeDegree.rootEntropyForm_shift line 26
lemma OAI.DukePrimeDegree.rootEntropyForm_indicator line 36
lemma OAI.DukePrimeDegree.rootEntropyForm_neg_indicator line 57
theorem OAI.DukePrimeDegree.balanced_of_rootEntropyForm_symmetry line 80
Source documentation
Trace-zero entropy symmetry implies the coefficient balance. The test weight is the indicator of one coordinate minus its average.
```
theorem balanced_of_rootEntropyForm_symmetry
    (w : ι → ι → ℝ)
    (hsym : ∀ t : ι → ℝ, ∑ i, t i = 0 →
      rootEntropyForm w t = rootEntropyForm w (fun i => -t i)) :
    ∀ a, ∑ j, w a j = ∑ j, w j a := by
…
```
Mentions: OAI.DukePrimeDegree.rootEntropyForm

theorem OAI.DukePrimeDegree.coefficients_symmetric_of_entropy_symmetry line 107

Source documentation

The purely finite part of EKL's coefficient symmetry conclusion.

theorem coefficients_symmetric_of_entropy_symmetry
    (w : ι → ι → ℝ) (hw : ∀ i j, 0 ≤ w i j)
    (hsym : ∀ t : ι → ℝ, ∑ i, t i = 0 →
      rootEntropyForm w t = rootEntropyForm w (fun i => -t i))
    (hcomp : ∀ a b c, a ≠ c → 0 < w a b → 0 < w b c → w a c = 1) :
    ∀ a b, w a b = w b a :=
…

Mentions: OAI.DukePrimeDegree.rootEntropyForm