OAI/NumberTheory/JointDickman/Analysis/MellinSieveIntegral.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The Mellin sieve profile: full integral and truncation error

  1. lemma OAI.JointDickman.mellinSieveFunction_atom line 10
  2. lemma OAI.JointDickman.integral_mellinSieveFunction line 19
  3. lemma OAI.JointDickman.mellinSieveFunction_tail_norm line 25
  4. lemma OAI.JointDickman.mellinSieveFunction_tail_integrable line 41
  5. lemma OAI.JointDickman.mellinSieveFunction_integrable line 55
  6. theorem OAI.JointDickman.mellinSieveFunction_integral_error line 75

    Source documentation

    Truncating the full transform beyond the profile's maximum costs only its elementary cubic tail.

    theorem mellinSieveFunction_integral_error {N B : ℝ} (hN : 0 < N) (hNB : N ≤ B) (t : ℝ) :
    ‖(∫ x in (0:ℝ)..B, mellinSieveFunction N t x) - mellinSieveMainKernel N t‖ ≤
      N^3/(2*B^2) := by
…

    Mentions: OAI.JointDickman.mellinSieveFunction, OAI.JointDickman.mellinSieveMainKernel