Coefficient-five reciprocal sieve on arbitrary natural intervals
ProvedOddGoldbach19.interval_reciprocal_weighted_sifted_fivegoldbachlarge-sievenumber-theory
The reciprocal weighted pair-sieve bound with denominator N+5qz holds for any finite set A contained in [M,M+N). Squarefree moduli q<=z contain1, z>=1, d is even, and no prime factor of any modulus divides n(n+d) for n in A.
Preamble
import Mathlib import Definitions.Def_TaoFivePrimes_SingularSeries open scoped BigOperators
Formal statement
theorem OddGoldbach19.interval_reciprocal_weighted_sifted_five
(Q : Finset ℕ+) (h1 : 1 ∈ Q) (M N d : ℕ) (z : ℝ) (hz : 1 ≤ z)
(hQ : ∀ q ∈ Q, Squarefree (q : ℕ) ∧ ((q : ℕ) : ℝ) ≤ z)
(hd : 2 ∣ d) (A : Finset ℕ) (hAN : A ⊆ Finset.Ico M (M + N))
(hA : ∀ q ∈ Q, ∀ n ∈ A, ∀ p ∈ (q : ℕ).primeFactors, ¬ p ∣ n*(n+d)) :
(A.card : ℝ) ≤ (∑ q ∈ Q,
(∏ p ∈ (q : ℕ).primeFactors,
if p ∣ d then 1 / ((p : ℝ)-1) else 2 / ((p : ℝ)-2)) /
((N : ℝ)+5*((q : ℕ) : ℝ)*z))⁻¹ := by sorrySource
Interval translation adapted from public Apache2.0 Prove2Me accepted proof ef73b684-e41f-4ba6-be36-cd6b0bd75f07. Uses the new proved coefficient-five nonuniform large sieve and the existing primitive Fourier energy inequality.