Large sieve

TheoremThe Montgomery–Vaughan weighted Hilbert inequality#✓fully proved

Let \(\iota\) be a finite index set and for \(r \in \iota\) let \(x_r\) and \(\delta_r > 0\) be real numbers and \(z_r\) a complex number. Write \(\|t\|\) for the distance from a real number \(t\) to the nearest integer, and suppose that \(\delta_r \le \|x_r - x_s\|\) for all \(r \ne s\). Then

\[ \left| \sum_{r} \sum_{s \ne r} \frac{z_r \overline{z_s}}{\sin(\pi (x_r - x_s))} \right| \le \frac{3}{2} \sum_{r} \frac{|z_r|^2}{\delta_r}. \]

public theorem weightedHilbertCosecant {ι : Type*} [Fintype ι] [DecidableEq ι]
    (x δ : ι → ℝ) (z : ι → ℂ) (hδ : ∀ r, 0 < δ r)
    (hsep : ∀ r s, r ≠ s →
      δ r ≤ ‖((x r - x s : ℝ) : AddCircle (1 : ℝ))‖) :
    ‖∑ r, ∑ s ∈ Finset.univ.erase r,
        z r * conj (z s) / Real.sin (Real.pi * (x r - x s))‖ ≤
      3 / 2 * ∑ r, ‖z r‖ ^ 2 / δ r

Sources

• Montgomery–Vaughan (1974), Theorem 1, in its weighted circle form. The proof follows Yangjit, arXiv:2203.14950, lines 166–205, 209–462, and 596–640: Selberg's eigenvector identity, the Hermitian spectral theorem, and convex circle packing estimates for the one-pole and two-pole cosecant-square sums.

Used by 1

Used byThe Montgomery–Vaughan weighted large sieve

TheoremThe Montgomery–Vaughan weighted large sieve#✓fully proved

Let \(N\) be a natural number, let \(a_n\) be complex numbers, let \(\iota\) be a finite index set and for \(r \in \iota\) let \(x_r\) and \(\delta_r > 0\) be real numbers. Write \(\|t\|\) for the distance from a real number \(t\) to the nearest integer, and suppose that \(\delta_r \le \|x_r - x_s\|\) for all \(r \ne s\). Then

\[ \sum_{r} \left( N + \frac{3}{2 \delta_r} \right)^{-1} \left| \sum_{n=0}^{N-1} a_n e^{2 \pi i n x_r} \right|^2 \le \sum_{n=0}^{N-1} |a_n|^2. \]

public theorem weightedLargeSieve {ι : Type*} [Fintype ι]
    (N : ℕ) (x δ : ι → ℝ) (a : ℕ → ℂ) (hδ : ∀ r, 0 < δ r)
    (hsep : ∀ r s, r ≠ s →
      δ r ≤ ‖((x r - x s : ℝ) : AddCircle (1 : ℝ))‖) :
    ∑ r, (N + 3 / (2 * δ r))⁻¹ *
        ‖∑ n ∈ Finset.range N, a n *
          Complex.exp (((2 * Real.pi * (n * x r) : ℝ) : ℂ) * Complex.I)‖ ^ 2 ≤
      ∑ n ∈ Finset.range N, ‖a n‖ ^ 2

Sources

• Montgomery–Vaughan, The large sieve (1973), Theorem 1, equations (1.5)–(1.6) and (2.4), lines 227–321. The proof uses duality, the exact geometric sum, and weightedHilbertCosecant.

Uses 1 · Used by 1

Proof usesThe Montgomery–Vaughan weighted Hilbert inequality

Used byArithmetic large sieve for primes in a progression

TheoremArithmetic large sieve for primes in a progression#✓fully proved

Let \(N\), \(z\), \(q\) and \(a\) be natural numbers with \(z > 0\) and \(q > 0\), and let \(S\) be a finite set of natural numbers less than \(N\) such that for every \(n \in S\) the number \(qn + a\) is prime and greater than \(z\). Write \(\mu\) for the Möbius function and \(\varphi\) for Euler's totient function. Then

\[ \left(\sum_{r=1}^{z} \frac{\mu(r)^2}{\varphi(r)\,(N + 3rz/2)}\right) |S|^2 \le \frac{q}{\varphi(q)}\,|S|. \]

public theorem arithmeticLargeSieve_progression (N z q a : ℕ) (hz : 0 < z)
    (hq : 0 < q) (S : Finset ℕ) (hS : S ⊆ Finset.range N)
    (hprime : ∀ n ∈ S, (q * n + a).Prime)
    (hlarge : ∀ n ∈ S, z < q * n + a) :
    (∑ r ∈ Finset.Icc 1 z,
        ((N : ℝ) + 3 * (r : ℝ) * z / 2)⁻¹ *
          (((ArithmeticFunction.moebius r : ℤ) : ℝ) ^ 2 / Nat.totient r)) *
        S.card ^ 2 ≤ ((q : ℝ) / Nat.totient q) * S.card

Sources

• Montgomery–Vaughan, The large sieve (1973), Corollary 1 and Lemma 3, equations (2.7) and (3.2), lines 322–461. The Farey fractions are weighted by the denominator-dependent spacing from weightedLargeSieve.

Uses 1 · Used by 1

Proof usesThe Montgomery–Vaughan weighted large sieve

Used byBrun–Titchmarsh inequality

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.