OAI/NumberTheory/CubicMoment/Estimates/PrimeWeightVariation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Concrete total-variation control for rescaled prime weights and their Mellin twists. This is the cost in the proved Abel summation inequality.

  1. lemma OAI.CubicFirstMoment.rescaled_mellin_deriv_bound line 12
  2. lemma OAI.CubicFirstMoment.contDiffOn_rescaled_mellin line 32
  3. lemma OAI.CubicFirstMoment.rescaled_mellin_variation line 42