OAI/NumberTheory/DukePrimeDegree/Entropy/LowEntropyHeightObservation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Geometric future observations with a small-entropy level label

The countable observation is finite on compact height ranges and its whole-future fibers lie in triangular right orbits. Its height label can have arbitrarily small entropy at every finite truncation. No finite Shannon entropy of the complete countable observation is assumed.

  1. theorem OAI.DukePrimeDegree.exists_low_height_entropy_triangular_observation line 20