RoughDivisorBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The distinguished divisor is rough at a fixed power scale. On a squarefree product this gives a uniform number of possible distinguished divisors, stronger than the generic divisor bound for stopped beta.

theorem OAI.CubicFirstMoment.rough_primary_divisor_card line 15

theorem OAI.CubicFirstMoment.eventually_rough_primary_divisor_card line 44

Source documentation

One constant controls all possible rough distinguished divisors in the whole fixed norm envelope, regardless of the smaller bin primes.

theorem eventually_rough_primary_divisor_card {ξ C : ℝ} (hξ : 0 < ξ) (hC : 0 < C) :
    ∃ K : ℕ, ∀ᶠ X : ℝ in atTop, ∀ (R : Finset Eisenstein),
      (∀ r ∈ R, primary r) →
      (∀ r ∈ R, ∀ p ∈ primaryPrimeFactors r, X^ξ ≤ norm p) →
      ∀ b : Eisenstein, primary b → Squarefree b → norm b ≤ C*X →
        (R.filter (fun r => r ∣ b)).card ≤ K := by
…

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

theorem OAI.CubicFirstMoment.stoppedBeta_rough_bound line 61