Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.
Unconditional bounds derived from the prime theorem #
The general lemmas in LeanPool.KloostermanWeil.Weil.ChineseRemainderAndCompletion accept a
PrimeNondegenerateWeil proof explicitly. Here they are instantiated with
prime_bound; callers do not need to supply that argument.
theorem
KloostermanWeil.squarefreeUnitNumerator_bound
{q : ℕ}
[NeZero q]
(hsq : Squarefree q)
(a b : ZMod q)
(ha : IsUnit a)
:
Squarefree-modulus estimate for a unit numerator.
theorem
KloostermanWeil.reducedModulusSum_bound
{A q : ℕ}
(hq : 0 < q)
(hsq : Squarefree q)
(b : ZMod (reducedModulus A q))
:
‖kloostermanUnitSum (reducedModulus A q) (↑(reducedNumerator A q)) b‖ ≤ 2 ^ (reducedModulus A q).primeFactors.card * √↑(reducedModulus A q)
Bound on the sum at the reduced modulus, with no lifting assertion.
theorem
KloostermanWeil.centeredReducedIntervalSum_bound
{A q : ℕ}
(hq : 0 < q)
(hsq : Squarefree q)
(x : ZMod (reducedModulus A q))
(L : ℕ)
:
‖centeredIntervalSum (reducedModulus A q) (↑(reducedNumerator A q)) x L‖ ≤ 2 ^ (reducedModulus A q).primeFactors.card * √↑(reducedModulus A q) * (1 + Real.log ↑(reducedModulus A q))
Centered completion on the reduced squarefree modulus.
theorem
KloostermanWeil.weightedCenteredReducedIntervalSum_bound
{A q : ℕ}
(hq : 0 < q)
(hsq : Squarefree q)
(x : ZMod (reducedModulus A q))
(Y L : ℕ)
(hY : 0 < Y)
:
‖weightedCenteredIntervalSum (reducedModulus A q) (↑(reducedNumerator A q)) x Y L‖ ≤ 2 * (2 ^ (reducedModulus A q).primeFactors.card * √↑(reducedModulus A q) * (1 + Real.log ↑(reducedModulus A q))) / ↑Y
Weighted centered completion with positive initial weight Y.