OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternGoodIdealIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original outer cutoff and regular density in the good matching estimate

  1. theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_good_ideal_integral_rate_window line 15