OAI/NumberTheory/JointDickman/Amplification/SingularSeries.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The singular series produced by the Ramanujan residue factor

  1. def OAI.JointDickman.singularSeriesCoefficient line 14
  2. def OAI.JointDickman.singularSeries line 17
  3. theorem OAI.JointDickman.singularSeriesCoefficient_one line 20
  4. theorem OAI.JointDickman.singularSeriesCoefficient_mul line 23
  5. theorem OAI.JointDickman.singularSeriesCoefficient_norm_le line 31
  6. theorem OAI.JointDickman.singularSeriesCoefficient_summable line 41
  7. theorem OAI.JointDickman.singularSeriesCoefficient_prime_power_zero line 47
  8. theorem OAI.JointDickman.singularSeries_local_factor line 54
  9. theorem OAI.JointDickman.singularSeries_hasProd line 74
  10. theorem OAI.JointDickman.singularSeries_local_bounds line 88
  11. theorem OAI.JointDickman.singularSeries_bounds line 100
  12. theorem OAI.JointDickman.singularSeries_eulerProduct line 115
  13. theorem OAI.JointDickman.singularSeries_eq_zero_of_odd line 120