Finite Fourier completion of the reciprocal sum

The modulus is any positive natural number, including one. Neither frequency is assumed coprime to it. These are finite identities and bounds, not an assertion of the complete Kloosterman square-root estimate.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase (q : ℕ) [NeZero q] (d : ℤ) (u : ZMod q) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase q d u = if IsUnit u then ZMod.stdAddChar (↑d * u⁻¹) else 0

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman (q : ℕ) [NeZero q] (m : ZMod q) (d : ℤ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman q m d = ∑ u : ZMod q, ZMod.stdAddChar (m * u) * MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase q d u

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.incompleteReciprocal (q : ℕ) [NeZero q] (d A : ℤ) (L : ℕ) : ℂ

The integers in the interval are A, A+1, ..., A+L-1.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.incompleteReciprocal q d A L = ∑ j ∈ Finset.range L, MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase q d (↑A + ↑j)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.intervalFourier (q : ℕ) [NeZero q] (A : ℤ) (L : ℕ) (m : ZMod q) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.intervalFourier q A L m = ∑ j ∈ Finset.range L, ZMod.stdAddChar (m * (↑A + ↑j))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_eq {q : ℕ} [NeZero q] (m : ZMod q) (d : ℤ) : completeKloosterman q m d = ∑ u : ZMod q, if IsUnit u then ZMod.stdAddChar (m * u + ↑d * u⁻¹) else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dft_reciprocalPhase {q : ℕ} [NeZero q] (d : ℤ) (m : ZMod q) : ZMod.dft (reciprocalPhase q d) m = completeKloosterman q (-m) d

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reciprocalPhase_fourier {q : ℕ} [NeZero q] (d : ℤ) (u : ZMod q) : reciprocalPhase q d u = (↑q)⁻¹ * ∑ m : ZMod q, ZMod.stdAddChar (m * u) * completeKloosterman q (-m) d

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.incompleteReciprocal_completion {q : ℕ} [NeZero q] (d A : ℤ) (L : ℕ) : incompleteReciprocal q d A L = (↑q)⁻¹ * ∑ m : ZMod q, intervalFourier q A L m * completeKloosterman q (-m) d

Exact completion, even for intervals longer than a period.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stdAddChar_norm {q : ℕ} [NeZero q] (u : ZMod q) : ‖ZMod.stdAddChar u‖ = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.intervalFourier_zero {q : ℕ} [NeZero q] (A : ℤ) (L : ℕ) : intervalFourier q A L 0 = ↑L

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.intervalFourier_norm_le_length {q : ℕ} [NeZero q] (A : ℤ) (L : ℕ) (m : ZMod q) : ‖intervalFourier q A L m‖ ≤ ↑L

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.intervalFourier_eq_geom {q : ℕ} [NeZero q] (A : ℤ) (L : ℕ) (m : ZMod q) : intervalFourier q A L m = ZMod.stdAddChar (m * ↑A) * ∑ j ∈ Finset.range L, ZMod.stdAddChar m ^ j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.intervalFourier_norm_mul {q : ℕ} [NeZero q] (A : ℤ) (L : ℕ) (m : ZMod q) : ‖intervalFourier q A L m‖ * ‖ZMod.stdAddChar m - 1‖ ≤ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.incompleteReciprocal_norm_le_completion {q : ℕ} [NeZero q] (d A : ℤ) (L : ℕ) (B : ℝ) (hB : ∀ (m : ZMod q), ‖completeKloosterman q m d‖ ≤ B) : ‖incompleteReciprocal q d A L‖ ≤ ((↑q)⁻¹ * ∑ m : ZMod q, ‖intervalFourier q A L m‖) * B

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.completeKloosterman_modulus_one (m : ZMod 1) (d : ℤ) : completeKloosterman 1 m d = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.incompleteReciprocal_modulus_one (d A : ℤ) (L : ℕ) : incompleteReciprocal 1 d A L = ↑L

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.incompleteReciprocal_zero_frequency {q : ℕ} [NeZero q] (A : ℤ) (L : ℕ) : incompleteReciprocal q 0 A L = ↑{j ∈ Finset.range L | IsUnit (↑A + ↑j)}.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.stdAddChar_sub_one_lower {q : ℕ} [NeZero q] (k : ℕ) (hk : k ≤ q) : 4 * min (↑k) (↑q - ↑k) ≤ ↑q * ‖ZMod.stdAddChar ↑k - 1‖

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.intervalFourier_norm_le_reciprocals {q : ℕ} [NeZero q] (A : ℤ) (L k : ℕ) (hk0 : 0 < k) (hkq : k < q) : ‖intervalFourier q A L ↑k‖ ≤ ↑q * ((↑k)⁻¹ + (↑(q - k))⁻¹)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.intervalFourier_lone {q : ℕ} [NeZero q] (A : ℤ) (L : ℕ) (hL : L ≤ q) : ∑ m : ZMod q, ‖intervalFourier q A L m‖ ≤ ↑q * (3 + 2 * Real.log ↑q)

The normalized interval Fourier L1 norm costs only one logarithm.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.incompleteReciprocal_norm_le_log {q : ℕ} [NeZero q] (d A : ℤ) (L : ℕ) (hL : L ≤ q) (B : ℝ) (hB : ∀ (m : ZMod q), ‖completeKloosterman q m d‖ ≤ B) : ‖incompleteReciprocal q d A L‖ ≤ (3 + 2 * Real.log ↑q) * B