OAI/NumberTheory/CubicMoment/Estimates/PrimeDetectorCutoff.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An explicit smooth cutoff for the exact prime detector.

  1. def OAI.CubicFirstMoment.primeDetectorCutoff line 13
  2. lemma OAI.CubicFirstMoment.primeDetectorCutoff_nonneg line 15
  3. lemma OAI.CubicFirstMoment.primeDetectorCutoff_le_one line 18
  4. lemma OAI.CubicFirstMoment.primeDetectorCutoff_one line 22
  5. lemma OAI.CubicFirstMoment.primeDetectorCutoff_zero line 25
  6. lemma OAI.CubicFirstMoment.primeDetectorCutoff_smooth line 28
  7. theorem OAI.CubicFirstMoment.concrete_prime_detector line 31