SmoothRankinSaving.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth-number discard on the exp(sqrt(log X)) scale. Only the ordinary prime number theorem is used.

lemma OAI.CubicFirstMoment.primaryPrime_reciprocal_exp_bound line 13
lemma OAI.CubicFirstMoment.exp_rankin_absorption line 37
theorem OAI.CubicFirstMoment.smooth_squarefree_log_saving line 62

theorem OAI.CubicFirstMoment.smooth_squarefree_discard line 111

Source documentation

The manuscript's actual long-prime cutoff. The exponent D is arbitrary, so this discards the terms having no prime above exp(sqrt(log X)).

theorem smooth_squarefree_discard (hpnt : PrimaryPrimePNT)
    {κ D : ℝ} (hκ : 0 < κ) :
    ∀ᶠ X : ℝ in atTop, ∀ (B : ℝ) (S : Finset Eisenstein),
      X^κ ≤ B →
      (∀ b ∈ S, primary b ∧ Squarefree b) →
      (∀ b ∈ S, norm b ≤ B) →
      (∀ b ∈ S, ∀ p ∈ primaryPrimeFactors b,
        norm p ≤ Real.exp (Real.sqrt (Real.log X))) →
      (S.card:ℝ) ≤ B*(Real.log X)^(-D) := by
…

Mentions: OAI.CubicFirstMoment.PrimaryPrimePNT, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryPrimeFactors