Replacing the retained ceiling cutoff by the floor cutoff

The ceiling cutoff is adequate for a tail estimate, but does not bound the dimensionless frequencies retained inside the Fourier integral. We replace the actual signed masked finite sum, and estimate its change before any supremum. The sharper tail estimate uses the first omitted integer, not the last retained integer. All constants are independent of the arithmetic mask and residue.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff (M Z : ℝ) (q r : ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff M Z q r = ⌊↑(q.lcm r) / M * Z⌋₊

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff_le_uniformCutoff (M Z : ℝ) (q r : ℕ) : wFloorCutoff M Z q r ≤ wUniformCutoff M Z q r

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff_scale {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {q r : ℕ} (hl : 0 < q.lcm r) : M / ↑(q.lcm r) * ↑(wFloorCutoff M Z q r) ≤ Z

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff_retained_scale {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {q r : ℕ} (hl : 0 < q.lcm r) {h : ℤ} (hh : h.natAbs ≤ wFloorCutoff M Z q r) : M * |↑h| / ↑(q.lcm r) ≤ Z

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff_mem_Icc_scale {M Z : ℝ} (hM : 0 < M) (hZ : 0 ≤ Z) {q r : ℕ} (hl : 0 < q.lcm r) {h : ℤ} (hh : h ∈ Finset.Icc (-↑(wFloorCutoff M Z q r)) ↑(wFloorCutoff M Z q r)) : M * |↑h| / ↑(q.lcm r) ≤ Z

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFloorCutoff_first_omitted_scale {M : ℝ} (hM : 0 < M) (Z : ℝ) {q r : ℕ} (hl : 0 < q.lcm r) : Z < M / ↑(q.lcm r) * (↑(wFloorCutoff M Z q r) + 1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dyadicPoissonTail_first_omitted_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 + 1)) ^ k

The first omitted integer gives an extra mesh width in the denominator.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_floorCutoff_error (k : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M Z : ℝ), 0 < M → 0 ≤ Z → ∀ (q r : ℕ) (a : ℤ) (n₁ n₂ H : ℕ), wFloorCutoff M Z q r ≤ 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 + Z) ^ k

Uniform truncation at any cutoff at least the floor, including zero moduli where the frequency summands vanish by definition.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_ceil_sub_floor_uniform (l : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M Z : ℝ), 0 < M → 0 ≤ Z → ∀ (N Q : Finset ℕ) (β c : ℕ → ℝ) (a : ℤ) (P : WOriginalTuple → Prop), |wMaskedTruncated M (wUniformCutoff M Z) N Q β c a P - wMaskedTruncated M (wFloorCutoff M Z) N Q β c a P| ≤ C * ((∑ q ∈ Q, |c q|) ^ 2 * (∑ n ∈ N, |β n|) ^ 2) / (1 + Z) ^ l

The actual retained sums are compared with identical signed coefficients and the identical arbitrary mask. No well-factorability input is used.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_ceil_sub_floor_fouvryTau (l : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M Z : ℝ), 0 < M → 0 < Z → ∀ (k j : ℕ), 1 ≤ k → 1 ≤ j → ∀ (T L : ℝ), 1 ≤ T → 1 ≤ L → ∀ (N Q : Finset ℕ), N ⊆ Finset.Ioc 0 ⌊T⌋₊ → Q ⊆ Finset.Ioc 0 ⌊L⌋₊ → ∀ (β c : ℕ → ℝ), (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ) (P : WOriginalTuple → Prop), |wMaskedTruncated M (wUniformCutoff M Z) N Q β c a P - wMaskedTruncated M (wFloorCutoff M Z) N Q β c a P| ≤ C * ((L * (1 + Real.log L) ^ (j - 1)) ^ 2 * (T * (1 + Real.log T) ^ (k - 1)) ^ 2) / Z ^ l

Fixed-order divisor means evaluate the actual ceiling-to-floor difference.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wMaskedTruncated_ceil_sub_floor_alpha_log_payment (i k j A : ℕ) {η : ℝ} (hη : 0 < η) : ∀ᶠ (x : ℝ) in Filter.atTop, ∀ (M : ℝ), 0 < M → ∀ (S N Q : Finset ℕ), S ⊆ Finset.Ioc 0 ⌊x⌋₊ → N ⊆ Finset.Ioc 0 ⌊x⌋₊ → Q ⊆ Finset.Ioc 0 ⌊x⌋₊ → ∀ (α β c : ℕ → ℝ), (∀ m ∈ S, |α m| ≤ ↑((fouvryTau i) m)) → (∀ n ∈ N, |β n| ≤ ↑((fouvryTau k) n)) → (∀ q ∈ Q, |c q| ≤ ↑((fouvryTau j) q)) → ∀ (a : ℤ) (P : WOriginalTuple → Prop), (∑ m ∈ S, α m ^ 2) * |wMaskedTruncated M (wUniformCutoff M (x ^ η)) N Q β c a P - wMaskedTruncated M (wFloorCutoff M (x ^ η)) N Q β c a P| ≤ x ^ 2 / Real.log x ^ A

The cutoff replacement is paid before choosing M, the signed data, the residue or the mask. The three fixed divisor orders may all be zero.