OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeCounting.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The short-interval prime-counting consequence needed for the weighted Halász mean-value argument, obtained by specializing the Brun--Titchmarsh sieve to modulus one.

  1. theorem OAI.TwoPointCorrelations.halasz_prime_interval_bound line 16

    Source documentation

    Uniform upper bound for any finite set of primes in a real interval. The location of the interval is unrestricted.

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimeCounting.lean:16 (same declaration text).

    theorem halasz_prime_interval_bound : ∃ C B : ℝ, 0 < C ∧ 1 < B ∧
    ∀ (x H : ℝ) (P : Finset ℕ), B ≤ H →
      (∀ p ∈ P, p.Prime ∧ x < (p : ℝ) ∧ (p : ℝ) ≤ x + H) →
      (P.card : ℝ) ≤ C * H / Real.log H := by
…