Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryLocalGlobal

From primitive prime powers to every nonzero modulus #

Chinese remaindering twists both frequencies by a Bezout coefficient. Its coprimality with the corresponding modulus preserves the full three-way gcd. Together with exact common-factor descent this proves the all-modulus estimate from a single explicitly quantified primitive prime-power input.

source
theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_bezout_coprime (m n : ℕ) (h : m.Coprime n) :
m.Coprime (m.gcdB n).natAbs ∧ n.Coprime (m.gcdA n).natAbs
Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_bezout_coprime · compiled type and proof/definition references.

source
theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_gcd_twist (q : ℕ) (b a d : ℤ) (hb : q.Coprime b.natAbs) :
q.gcd ((a * b).natAbs.gcd (d * b).natAbs) = q.gcd (a.natAbs.gcd d.natAbs)
Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_gcd_twist · compiled type and proof/definition references.

source
theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_gcd_coprime_mul (m n g : ℕ) (h : m.Coprime n) :
(m * n).gcd g = m.gcd g * n.gcd g
Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_gcd_coprime_mul · compiled type and proof/definition references.

source
theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_weil_envelope_mul (m n g : ℕ) (h : m.Coprime n) :
↑(m * n).divisors.card * √↑((m * n).gcd g) * √↑(m * n) = ↑m.divisors.card * √↑(m.gcd g) * √↑m * (↑n.divisors.card * √↑(n.gcd g) * √↑n)
Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.localGlobal_weil_envelope_mul · compiled type and proof/definition references.

source
theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_weil_of_primitive_prime_power (hlocal : ∀ (p k : ℕ) (x : Fact (Nat.Prime p)) (a d : ℤ), ¬↑p ∣ a ∨ ¬↑p ∣ d → ‖completeKloosterman (p ^ k) (↑a) d‖ ≤ ↑(k + 1) * √↑(p ^ k)) (q : ℕ) [NeZero q] (a d : ℤ) :
‖completeKloosterman q (↑a) d‖ ≤ ↑q.divisors.card * √↑(q.gcd (a.natAbs.gcd d.natAbs)) * √↑q

Conditional all-modulus Weil bound, with signed frequencies, modulus one, and zero or nonprimitive frequencies. Only primitive prime-power bounds are assumed; coprime assembly and common-factor descent are proved.

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_weil_of_primitive_prime_power · compiled type and proof/definition references.

source
theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_weil_zmod_of_primitive_prime_power (hlocal : ∀ (p k : ℕ) (x : Fact (Nat.Prime p)) (a d : ℤ), ¬↑p ∣ a ∨ ¬↑p ∣ d → ‖completeKloosterman (p ^ k) (↑a) d‖ ≤ ↑(k + 1) * √↑(p ^ k)) (q : ℕ) [NeZero q] (m : ZMod q) (d : ℤ) :
‖completeKloosterman q m d‖ ≤ ↑q.divisors.card * √↑(q.gcd (m.val.gcd d.natAbs)) * √↑q

The residue-valued interface used by the existing Weil-to-Fouvry bridge.

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_weil_zmod_of_primitive_prime_power · compiled type and proof/definition references.