OAI/NumberTheory/JointDickman/Analysis/MellinSieveGrid.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Direct divisor-grid approximation for the Mellin sieve kernel

  1. lemma OAI.JointDickman.sum_grid_eq_filter line 11
  2. lemma OAI.JointDickman.mellinSieve_grid_riemann line 35
  3. theorem OAI.JointDickman.mellinSieve_grid_error line 54

    Source documentation

    The low-frequency kernel error, with the actual rounded divisor-grid endpoint exposed. It is uniform in the divisor and in the frequency.

    theorem mellinSieve_grid_error {N : ℝ} (hN : 0 < N) (K d : ℕ) (hd : 0 < d)
    (hB : N ≤ (d:ℝ)*(K/d:ℕ)) (t : ℝ) :
    ‖mellinSieveDiscreteKernel K d N t-mellinSieveMainKernel N t/(d:ℂ)‖ ≤
      (K/d:ℕ)*(d:ℝ)*((3+|t|)/N) + N^3/((d:ℝ)*2*((d:ℝ)*(K/d:ℕ))^2) := by
…

    Mentions: OAI.JointDickman.mellinSieveDiscreteKernel, OAI.JointDickman.mellinSieveMainKernel