OAI/NumberTheory/Ostmann/ZeroDensity/RieszUnsmoothing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Recovering sharp positive counts from the integrated count

  1. def OAI.Ostmann.finiteRieszSum line 13
  2. theorem OAI.Ostmann.positivePart_step_lower line 16
  3. theorem OAI.Ostmann.positivePart_step_upper line 24
  4. theorem OAI.Ostmann.finiteRieszSum_step line 35