OAI/NumberTheory/DukePrimeDegree/Entropy/SmallHeightEntropy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coarse heights with uniformly small finite-observation entropy

A shift of a sufficiently coarse binning has rare changes. The ternary reconstruction bound therefore makes every finite truncation have small entropy rate, without any moment assumption on the original height.

  1. theorem OAI.DukePrimeDegree.exists_coarse_height_small_entropy line 19