OAI/NumberTheory/DukePrimeDegree/Entropy/RegularRootEntropyActual.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual regular entropy upper bound

The aperiodic case uses small complete orbit sections and actual quotient charts. The periodic case has zero entropy. Full diagonal ergodicity is used only for that dichotomy, never as ergodicity of the selected map.

  1. lemma OAI.DukePrimeDegree.measurableSet_aperiodic line 21
  2. theorem OAI.DukePrimeDegree.negative_diagonal_entropy_le_root_sum line 32