OAI/NumberTheory/TwoPoint/Bounds/SieveGoldbachLocal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The positive Euler factors of the actual binary Goldbach sieve.

  1. def OAI.TwoPointCorrelations.sieveGoldbachWeight line 13
  2. lemma OAI.TwoPointCorrelations.sieve_goldbach_density_lt_one line 16
  3. lemma OAI.TwoPointCorrelations.sieve_goldbach_weight_pos line 20
  4. lemma OAI.TwoPointCorrelations.sieve_goldbach_one_add line 25
  5. lemma OAI.TwoPointCorrelations.sieve_goldbach_normalized line 32
  6. lemma OAI.TwoPointCorrelations.sieve_goldbach_mean_le line 40
  7. lemma OAI.TwoPointCorrelations.sieve_goldbach_factor_ge line 53