HalaszUnitPrimeWindows.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A fixed-width mean square for every finite prime set. The finitely many primes below the sieve threshold cost only an absolute constant.

lemma OAI.TwoPointCorrelations.halasz_prime_fixed_rows line 14
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitPrimeWindows.lean:14 (same declaration text).

theorem OAI.TwoPointCorrelations.halasz_prime_mean_square_unit line 65

Source documentation

The unit-interval prime mean square, with no lower prime cutoff.

Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszUnitPrimeWindows.lean:65 (same declaration text).

theorem halasz_prime_mean_square_unit : ∃ C : ℝ, 0 < C ∧
    ∀ (P : Finset ℕ), (∀ p ∈ P, p.Prime) → ∀ (a : ℕ → ℂ) (u : ℝ),
      (∫ t in (u - 1 / 2)..(u + 1 / 2),
        ‖mrtExponentialPolynomial P
          (fun p => a p * ((Real.log (p : ℝ) / p : ℝ) : ℂ))
          (fun p => -Real.log (p : ℝ)) t‖ ^ 2) ≤
        C * ∑ p ∈ P, ‖a p‖ ^ 2 * (Real.log (p : ℝ) / p) := by
…

Mentions: OAI.TwoPointCorrelations.mrtExponentialPolynomial