OAI/NumberTheory/CubicMoment/Estimates/DivisorCharacterMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact divisor mass behind the genuine coprimality kernel, with arbitrary squarefree coefficients and both Fourier signs.

  1. def OAI.CubicFirstMoment.divisorCharacterMass line 14
  2. lemma OAI.CubicFirstMoment.divisorCharacterMass_continuous line 17
  3. lemma OAI.CubicFirstMoment.divisorCharacterMass_bound line 22
  4. lemma OAI.CubicFirstMoment.twistedCoprimeMellinMass_eq_divisor_mass line 32