The exact interval and gcd form of the conditional Weil-to-Fouvry bridge

The complete Kloosterman estimate is an explicit hypothesis, not a proved input. The interval conversion and the divisor/logarithm payment are proved.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalInterval (q : ℕ) [NeZero q] (d : ℤ) (X Y : ℝ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalInterval q d X Y = ∑ c ∈ Finset.Ioc ⌊X⌋ ⌊Y⌋, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase q d ↑c

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalInterval_eq_coprime_sum {q : ℕ} [NeZero q] (d : ℤ) (X Y : ℝ) : reciprocalInterval q d X Y = ∑ c ∈ Finset.Ioc ⌊X⌋ ⌊Y⌋ with IsCoprime (↑q) c, ZMod.stdAddChar (↑d * (↑c)⁻¹)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_reciprocalInterval (c : ℤ) (X Y : ℝ) : c ∈ Finset.Ioc ⌊X⌋ ⌊Y⌋ ↔ X < ↑c ∧ ↑c ≤ Y

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalInterval_eq_incomplete {q : ℕ} [NeZero q] (d : ℤ) {X Y : ℝ} (hXY : X ≤ Y) : reciprocalInterval q d X Y = incompleteReciprocal q d (⌊X⌋ + 1) (⌊Y⌋ - ⌊X⌋).toNat

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalInterval_length_le {q : ℕ} {X Y : ℝ} (h : Y - X ≤ ↑q) : (⌊Y⌋ - ⌊X⌋).toNat ≤ q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau_pow_pointwise (k r : ℕ) (hk : 1 ≤ k) {n : ℕ} (hn : 0 < n) : ↑((fouvryTau k) n) ^ r ≤ ↑n * (1 + Real.log ↑n) ^ (k ^ r - 1)

A pointwise fixed-order moment bound extracted from the proved full mean.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.eventually_divisors_completion_loss {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑n.divisors.card * (3 + 2 * Real.log ↑n) ≤ ↑n ^ ε

Arbitrarily high fixed moments pay the exact divisor/logarithm completion loss. The threshold is uniform in the positive integer argument.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.divisors_completion_loss {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 0 < n → ↑n.divisors.card * (3 + 2 * Real.log ↑n) ≤ C * ↑n ^ ε

A single constant covers all moduli, not merely sufficiently large ones.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_gcd_envelope {q : ℕ} [NeZero q] (d : ℤ) (hWeil : ∀ (m : ZMod q), ‖completeKloosterman q m d‖ ≤ ↑q.divisors.card * √↑(q.gcd (m.val.gcd d.natAbs)) * √↑q) (m : ZMod q) : ‖completeKloosterman q m d‖ ≤ ↑q.divisors.card * √↑(q.gcd d.natAbs) * √↑q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalInterval_weil_to_fouvry (hWeil : ∀ (q : ℕ) (x : NeZero q) (m : ZMod q) (d : ℤ), ‖completeKloosterman q m d‖ ≤ ↑q.divisors.card * √↑(q.gcd (m.val.gcd d.natAbs)) * √↑q) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℕ) (x : NeZero q) (d : ℤ) (X Y : ℝ), X ≤ Y → Y - X ≤ ↑q → ‖reciprocalInterval q d X Y‖ ≤ C * √↑(q.gcd d.natAbs) * ↑q ^ (1 / 2 + ε)

Exact F87 Lemma 3 interval and frequency domain, conditional ONLY on the complete Weil input, which remains an unproved external formalization frontier.