OAI/NumberTheory/Ostmann/ZeroDensity/DensityMollifierMean.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The mean square of the actual critical-line Möbius polynomial

  1. theorem OAI.Ostmann.densityMollifier_vertical line 12
  2. theorem OAI.Ostmann.density_mobius_half_energy line 24
  3. theorem OAI.Ostmann.critical_mollifier_mean line 43
  4. theorem OAI.Ostmann.density_divisor_half_energy line 58