Uniform rapid truncation of the retained Poisson series

The error constant depends only on the requested power and the fixed bump. The estimate remains uniform when the period exceeds the smoothing scale.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicPoissonTail (t x : ℝ) (H : ℕ) (h : ℤ) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicPoissonTail t x H h = if h.natAbs ≤ H then 0 else MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffPoissonRemainder t x h

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicPoissonTail_uniform (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 < t → ∀ (x : ℝ) (H : ℕ), (Summable fun (h : ℤ) => ‖dyadicPoissonTail t x H h‖) ∧ ‖∑' (h : ℤ), dyadicPoissonTail t x H h‖ ≤ C / (1 + t * ↑H) ^ k

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicPoissonRemainder_eq_truncation {t : ℝ} (ht : 0 < t) (x : ℝ) (H : ℕ) : ∑' (h : ℤ), dyadicCutoffPoissonRemainder t x h = ∑ h ∈ Finset.Icc (-↑H) ↑H, dyadicCutoffPoissonRemainder t x h + ∑' (h : ℤ), dyadicPoissonTail t x H h

Splitting off finitely many frequencies does not discard their phases.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_truncation_error (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (q r : ℕ), q ≠ 0 → r ≠ 0 → ∀ (a : ℤ) (n₁ n₂ H : ℕ), ‖∑' (h : ℤ), wPoissonFrequency M a q r n₁ n₂ h - ∑ h ∈ Finset.Icc (-↑H) ↑H, wPoissonFrequency M a q r n₁ n₂ h‖ ≤ C / (1 + M / ↑(q.lcm r) * ↑H) ^ k

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.truncatedWNonzeroMode (M : ℝ) (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) : ℝ

The finite oscillatory sum, with a separate cutoff for each modulus pair.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.truncatedWNonzeroMode M H N Q β c a = ∑ q ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ r ∈ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.reducedModuli Q a, ∑ n₁ ∈ N, ∑ n₂ ∈ N, if MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WCompatible q r n₁ n₂ then c q * c r * β n₁ * β n₂ * (∑ h ∈ Finset.Icc (-↑(H q r)) ↑(H q r), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency M a q r n₁ n₂ h).re else 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.smoothWNonzeroMode_truncation_error (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : ℝ), 0 < M → ∀ (H : ℕ → ℕ → ℕ) (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ), (∀ q ∈ Q, q ≠ 0) → |smoothWNonzeroMode M N Q β c a - truncatedWNonzeroMode M H N Q β c a| ≤ C * ∑ q ∈ reducedModuli Q a, ∑ r ∈ reducedModuli Q a, ∑ n₁ ∈ N, ∑ n₂ ∈ N, if WCompatible q r n₁ n₂ then |c q * c r * β n₁ * β n₂| / (1 + M / ↑(q.lcm r) * ↑(H q r)) ^ k else 0

A quantitative truncation of the actual W remainder. No cancellation of the retained finite Kloosterman-type sum is assumed.