HalaszPrimeCounting.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

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

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/TwoPointCorrelations/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
…
```