OAI/NumberTheory/JointDickman/Analysis/MellinSieveProfile.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A positive smooth weight for sparse prime sampling

The weight is at least 1/8 on [N,2N] and its Mellin transform has quadratic decay. This provides the majorant used by the finite sieve.

  1. def OAI.JointDickman.mellinSieveWeight line 14
  2. def OAI.JointDickman.mellinSieveAtom line 17
  3. lemma OAI.JointDickman.mellinSieveWeight_nonneg line 21
  4. lemma OAI.JointDickman.mellinSieveWeight_left line 26
  5. lemma OAI.JointDickman.mellinSieveWeight_right line 36
  6. lemma OAI.JointDickman.mellinSieveWeight_interval line 47
  7. lemma OAI.JointDickman.mellinSieveAtom_log line 56
  8. theorem OAI.JointDickman.integral_mellinSieveAtom line 66

    Source documentation

    The positive weight has an exact quadratic-decay Mellin transform.

    theorem integral_mellinSieveAtom (N t : ℝ) :
    (∫ x in Set.Ioi (0 : ℝ), mellinSieveAtom N t x) =
      ((4*N/(4+t^2) : ℝ) : ℂ) := by
…

    Mentions: OAI.JointDickman.mellinSieveAtom