OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupTailNumerical.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform elementary sieve gap for conductor up to N^(19/20). The root variables isolate the algebra: p=P^(1/3), q=Q^(1/3), r=N^(1/120). Only one cubic orientation and the ordinary sieve are needed.

  1. lemma OAI.CubicFirstMoment.primeGroupTail_polynomial_min line 11
  2. lemma OAI.CubicFirstMoment.primeGroupTail_sieve_min line 72

    Source documentation

    Below conductor N^(19/20), the two relevant sieve bounds have an absolute gap, apart from the explicit ordinary-sieve diagonal N.

    lemma primeGroupTail_sieve_min {P Q N : ℝ}
    (hP : 1 ≤ P) (hQ : 1 ≤ Q) (hN : 1 ≤ N) (hD : P*Q^2 ≤ N^(19/20:ℝ)) :
    min (Q*(P+N+(P*N)^(2/3:ℝ))) ((P*Q)^2+N) ≤
      N+3*N^(119/120:ℝ)*(P*Q^2)^(1/3:ℝ) := by
…