Poisson extraction for the fixed dyadic cutoff

The period and the shift are arbitrary. The error constant is chosen before the scale, period, and shift, including when the period exceeds the scale.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_poisson_rescaled {M D : ℝ} (hM : 0 < M) (hD : 0 < D) (b : ℝ) : ∑' (z : ℤ), ↑(scaledDyadicCutoff M (b + D * ↑z)) = ∑' (h : ℤ), (M / D) • (FourierTransform.fourier dyadicCutoffSchwartz) (M / D * ↑h) * (fourier h) ↑(b / D)

Poisson summation on a real affine lattice, in the rescaled unit-period form.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_poisson {M D : ℝ} (hM : 0 < M) (hD : 0 < D) (b : ℝ) : ∑' (z : ℤ), ↑(scaledDyadicCutoff M (b + D * ↑z)) = D⁻¹ • ∑' (h : ℤ), FourierTransform.fourier (fun (x : ℝ) => ↑(scaledDyadicCutoff M x)) (↑h / D) * (fourier h) ↑(b / D)

The affine-lattice Poisson formula with the Fourier transform at h / D. The positive Fourier phase is Mathlib's fourier h (b / D).

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.poisson_decay_step {t : ℝ} (ht : 0 < t) (n : ℕ) : t / (1 + t * (↑n + 1)) ^ 2 ≤ 1 / (1 + t * ↑n) - 1 / (1 + t * (↑n + 1))

A telescoping majorant that remains bounded when the mesh tends to zero.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.poisson_decay_sum_range_le {t : ℝ} (ht : 0 < t) (N : ℕ) : ∑ n ∈ Finset.range N, t / (1 + t * (↑n + 1)) ^ 2 ≤ 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.poisson_decay_summable_nat {t : ℝ} (ht : 0 < t) : Summable fun (n : ℕ) => t / (1 + t * (↑n + 1)) ^ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.poisson_decay_tsum_nat_le {t : ℝ} (ht : 0 < t) : ∑' (n : ℕ), t / (1 + t * (↑n + 1)) ^ 2 ≤ 1

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.poissonNonzeroDecay (t : ℝ) (h : ℤ) : ℝ

The decay majorant with the main (zero-frequency) term removed.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.poissonNonzeroDecay t h = if h = 0 then 0 else t / (1 + |t * ↑h|) ^ 2

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.poissonNonzeroDecay_summable_tsum_le {t : ℝ} (ht : 0 < t) : Summable (poissonNonzeroDecay t) ∧ ∑' (h : ℤ), poissonNonzeroDecay t h ≤ 2

Both halves of the nonzero integer lattice have mass at most one.

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

The nonzero-frequency part of the rescaled Poisson series.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffPoissonRemainder t x h = if h = 0 then 0 else t • (FourierTransform.fourier MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffSchwartz) (t * ↑h) * (fourier h) ↑x

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicCutoffPoissonRemainder_uniform : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 < t → ∀ (x : ℝ), (Summable fun (h : ℤ) => ‖dyadicCutoffPoissonRemainder t x h‖) ∧ ‖∑' (h : ℤ), dyadicCutoffPoissonRemainder t x h‖ ≤ C

Uniform absolute control of the Fourier remainder. The same constant works for every positive mesh and every real shift.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_poisson_mainTerm {M D : ℝ} (hM : 0 < M) (hD : 0 < D) (b : ℝ) : ∑' (z : ℤ), ↑(scaledDyadicCutoff M (b + D * ↑z)) - (M / D) • (FourierTransform.fourier dyadicCutoffSchwartz) 0 = ∑' (h : ℤ), dyadicCutoffPoissonRemainder (M / D) (b / D) h

Exact extraction of the zero frequency from the affine-lattice formula.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.scaledDyadicCutoff_poisson_uniform_error : ∃ (C : ℝ), 0 < C ∧ ∀ (M D : ℝ), 0 < M → 0 < D → ∀ (b : ℝ), ‖∑' (z : ℤ), ↑(scaledDyadicCutoff M (b + D * ↑z)) - (M / D) • (FourierTransform.fourier dyadicCutoffSchwartz) 0‖ ≤ C

The fixed cutoff has a universal O(1) progression error. In particular, there is no restriction D ≤ M and the constant does not depend on the shift.