OAI/NumberTheory/CubicMoment/Angular/AngularKummerWeightVariation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Dividing a smooth prime weight by log preserves an explicit finite variation bound above exp(1). This removes the Chebyshev weight without assuming any weighted prime estimate.

  1. lemma OAI.CubicFirstMoment.prime_log_weight_deriv_bound line 14
  2. lemma OAI.CubicFirstMoment.log_normalized_rescaled_mellin_variation line 43
  3. theorem OAI.CubicFirstMoment.scaled_angular_kummer_prime_bound line 115