OAI/NumberTheory/Ostmann/ZeroDensity/DensityDivisorMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The elementary second moment of divisor coefficients

Pairs of divisors are counted by their least common multiple. The harmonic-cube estimate gives the logarithmic third power without a pointwise divisor bound.

  1. theorem OAI.Ostmann.density_divisor_count_as_sum line 17
  2. theorem OAI.Ostmann.density_divisor_square_as_sum line 32
  3. theorem OAI.Ostmann.density_divisor_square_sum line 43