OAI/NumberTheory/DukePrimeDegree/Geometry/RootPairSourceSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A positive-measure source for synchronized recurrence

The maximal estimates leave positive measure whenever their explicit error budget is below one. Any prescribed null set can be removed without losing positivity or the simultaneous recurrence and covariance properties.

  1. theorem OAI.DukePrimeDegree.exists_positive_rootPair_source_set line 21