OAI/NumberTheory/Ostmann/Construction/SmoothPrimeMeanTest.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A fixed smooth test for the prime mean of the sparse weight

  1. def OAI.Ostmann.primeMeanTest line 12
  2. theorem OAI.Ostmann.primeMeanTest_nonneg line 14
  3. theorem OAI.Ostmann.primeMeanTest_le_one line 16
  4. theorem OAI.Ostmann.primeMeanTest_contDiff line 18
  5. theorem OAI.Ostmann.primeMeanTest_zero_outside line 21
  6. theorem OAI.Ostmann.primeMeanTest_compactSupport line 28
  7. theorem OAI.Ostmann.primeMeanTest_center line 31
  8. theorem OAI.Ostmann.primeMeanTest_integral_pos line 35
  9. def OAI.Ostmann.primeMeanMellin line 41
  10. def OAI.Ostmann.smoothMangoldtMean line 45