HalaszPrimeMeanSquare.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A prime-supported mean-value theorem with one von Mangoldt weight, proved from the Brun--Titchmarsh theorem and the exact Fourier kernel. This is the sparse mean-square input to Halasz's argument.

theorem OAI.TwoPointCorrelations.halasz_prime_mean_square line 16

Source documentation

Arbitrary complex prime coefficients are permitted. The constant is independent of the upper end of the finite prime set.

Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeMeanSquare.lean:16 (same declaration text).

theorem halasz_prime_mean_square : ∃ C B : ℝ, 0 < C ∧ 2 ≤ B ∧
    ∀ (T : ℝ) (P : Finset ℕ), B ≤ T →
      (∀ p ∈ P, p.Prime ∧ T ^ 2 ≤ (p : ℝ)) → ∀ a : ℕ → ℂ,
      (∫ t in -T..T,
        ‖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