OAI/NumberTheory/Ostmann/Arithmetic/MovingOuterHaarComparison.lean
2 declarations, 0 contain sorry, 0 declared as axioms
The original outer-prior comparisons as corrected Haar integrals
- theorem
OAI.Ostmann.PublishedProgressionInput.moving_outer_prime_haar_rateline 13 - theorem
OAI.Ostmann.PublishedProgressionInput.moving_outer_mixed_haar_rateline 68