OAI/NumberTheory/CubicMoment/Estimates/ScaledPrimeInput.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A rescaled, Mellin-twisted prime estimate derived from the precise published unweighted Siegel–Walfisz input.

  1. lemma OAI.CubicFirstMoment.continuous_zero_on_lower_closed line 13
  2. def OAI.CubicFirstMoment.smoothPrimeCharacterSum line 20
  3. lemma OAI.CubicFirstMoment.smoothPrimeCharacterSum_eq_interval line 23
  4. theorem OAI.CubicFirstMoment.scaled_cubic_prime_bound line 39