OAI/NumberTheory/Ostmann/ZeroDensity/DensitySmoothedKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The normalized right-hand kernel in the square functional equation

  1. def OAI.Ostmann.densitySquareKernel line 12
  2. theorem OAI.Ostmann.densitySmoothedSquare_integral line 15
  3. theorem OAI.Ostmann.densitySquareKernel_line_bound line 31
  4. theorem OAI.Ostmann.densitySquareKernel_line_continuous line 45