OAI/NumberTheory/DukePrimeDegree/Entropy/CompactSmallObservations.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Finite observations with uniformly small lifts on a compact set
- theorem
OAI.DukePrimeDegree.exists_finite_observation_small_liftsline 14