OAI/NumberTheory/TwoPoint/Bounds/SievePrimeEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Prime additive energy from the finite Goldbach sieve and the singular-factor mean square.

  1. lemma OAI.TwoPointCorrelations.sieve_prime_pair_card line 14
  2. lemma OAI.TwoPointCorrelations.sieve_prime_sum_even line 32
  3. theorem OAI.TwoPointCorrelations.sieve_prime_additive_energy line 41

    Source documentation

    The number of zero-sum prime quadruples has the required four logarithms uniformly for every finite prime set below twice the scale.

    theorem sieve_prime_additive_energy :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ x : ℝ in atTop, ∀ P : Finset ℕ,
      (∀ p ∈ P, p.Prime ∧ p ≠ 2 ∧ (p : ℝ) ≤ 2 * x) →
      (Finset.addEnergy P P : ℝ) ≤ C * x ^ 3 / Real.log x ^ 4 := by
…