OAI/NumberTheory/JointDickman/Probability/WeightedRationalKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A quantitative totient-weighted rational geometric-kernel bound

  1. lemma OAI.JointDickman.rational_progression_weighted_bound line 11
  2. theorem OAI.JointDickman.totient_weighted_rational_kernel_bound line 43

    Source documentation

    This bound allows an extra logarithm in the rational denominator, which is harmless for the polylogarithmic minor arcs used in this application.

    theorem totient_weighted_rational_kernel_bound (q : ℕ) (hq : 0 < q)
    (a : ℕ) (ha : a.Coprime q) (N X : ℕ) :
    (∑ h ∈ Ioc 0 X, ((h:ℝ)/h.totient)*geometricSquareKernel N ((a:ℝ)/q*h)) ≤
      2*Real.exp 2 * ((N:ℝ)^2*X*(1+Real.log q)/q +
        (N:ℝ)*X + (N:ℝ)*q*(1+Real.log X)) := by
…

    Mentions: OAI.JointDickman.geometricSquareKernel