SparseDivisorRankin.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal mass of large squarefree divisors composed only of polylogarithmically small primes. This is the Rankin step for sparse late stops in the prime decomposition, derived from ordinary prime counting.

lemma OAI.CubicFirstMoment.squarefree_reciprocal_rankin_tail line 14
lemma OAI.CubicFirstMoment.prime_shifted_reciprocal_sum line 36
lemma OAI.CubicFirstMoment.power_log_sublinear line 51

theorem OAI.CubicFirstMoment.polylog_smooth_divisor_reciprocal_saving line 76

Source documentation

The precise sparse-divisor consequence needed for late stops. The exponent depends on the fixed prime cutoff power and divisor size.

theorem polylog_smooth_divisor_reciprocal_saving
    (hpnt : PrimaryPrimePNT) {C η : ℝ} (hC : 0 < C) (hη : 0 < η) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ᶠ X : ℝ in atTop,
      ∀ S : Finset Eisenstein,
      (∀ d ∈ S, primary d ∧ Squarefree d) →
      (∀ d ∈ S, X^η ≤ norm d) →
      (∀ d ∈ S, ∀ p ∈ primaryPrimeFactors d, norm p ≤ (Real.log X)^C) →
      (∑ d ∈ S, (norm d)⁻¹) ≤ X^(-δ) := by
…

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