SmallBConductorNumerical.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform elementary sieve gap below the exceptional conductor scale. The root variables isolate the algebra: p=P^(1/3), q=Q^(1/3), r=N^(1/24). Only one cubic orientation and the ordinary sieve are needed.

lemma OAI.CubicFirstMoment.small_conductor_polynomial_min line 11

lemma OAI.CubicFirstMoment.small_conductor_sieve_min line 72

Source documentation

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

lemma small_conductor_sieve_min {P Q N : ℝ}
    (hP : 1 ≤ P) (hQ : 1 ≤ Q) (hN : 1 ≤ N) (hD : P*Q^2 ≤ N^(3/4:ℝ)) :
    min (Q*(P+N+(P*N)^(2/3:ℝ))) ((P*Q)^2+N) ≤
      N+3*N^(23/24:ℝ)*(P*Q^2)^(1/3:ℝ) := by
…