OAI/NumberTheory/JointDickman/Amplification/WeightedCountTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Markov bounds for prime counts in the actual coefficient sums

  1. theorem OAI.JointDickman.weighted_exp_markov line 11
  2. def OAI.JointDickman.tripleCoefficientWeight line 30
  3. def OAI.JointDickman.triplePrimeCount line 33
  4. theorem OAI.JointDickman.coefficient_form_exp_moment line 39
  5. theorem OAI.JointDickman.coefficient_form_count_tail line 67