OAI/NumberTheory/DukePrimeDegree/Entropy/SparseFineObservation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Low-entropy fine observations without map ergodicity

Small complete sections at all precisions give arbitrarily fine future returns. Only the aperiodicity of the points in the prescribed chart is used; the selected transformation need not be ergodic.

  1. theorem OAI.DukePrimeDegree.exists_sparse_fine_future_observation line 22