OAI/NumberTheory/Ostmann/QuadraticCenter/PrimeDivisorMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A small weighted mass for the primes dividing one integer

  1. theorem OAI.Ostmann.prime_log_weight_le_one line 12
  2. theorem OAI.Ostmann.prime_divisor_mass_bound line 25

    Source documentation

    Splitting at the integer Y costs at most Y from small primes and log(D)/Y from the remaining divisors. Taking Y near sqrt(log D) suffices for the split-prime application.

    theorem prime_divisor_mass_bound (P : Finset ℕ) (D Y : ℕ) (s : ℝ)
    (hP : ∀ p ∈ P, p.Prime) (hD : 0 < D) (hY : 0 < Y) (hs : 1 ≤ s) :
    (∑ p ∈ P.filter (fun p => p ∣ D), Real.log p / (p : ℝ) ^ s) ≤
      Y + Real.log D / Y := by
…