OAI/NumberTheory/TwoPoint/Bounds/SieveSingularAverage.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An absolute mean-square bound for the Goldbach singular factor.

  1. lemma OAI.TwoPointCorrelations.sieve_prime_sqrt_product line 14
  2. lemma OAI.TwoPointCorrelations.sieve_prime_divisor_subsum line 20
  3. lemma OAI.TwoPointCorrelations.sieve_singular_square_divisor line 42
  4. def OAI.TwoPointCorrelations.sieveSingularMeanConstant line 48
  5. lemma OAI.TwoPointCorrelations.sieve_singular_mean_constant_nonneg line 51
  6. theorem OAI.TwoPointCorrelations.sieve_singular_square_average line 57

    Source documentation

    An absolute mean square for the singular factor, with no distribution hypothesis on primes or on the target integer.

    theorem sieve_singular_square_average (N : ℕ) :
    (∑ n ∈ Icc 1 N, sieveSingularFactor n ^ 2) ≤ sieveSingularMeanConstant * N := by
…

    Mentions: OAI.TwoPointCorrelations.sieveSingularFactor, OAI.TwoPointCorrelations.sieveSingularMeanConstant