OAI/NumberTheory/JointDickman/Counting/SingularSeriesPeriodic.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A periodic finite-factor approximation to the lag singular series

  1. def OAI.JointDickman.periodicSingularSeries line 11
  2. theorem OAI.JointDickman.totientLocalProduct_modEq line 14
  3. theorem OAI.JointDickman.singularSeriesCoefficient_modEq line 22
  4. theorem OAI.JointDickman.periodicSingularSeries_modEq line 34
  5. theorem OAI.JointDickman.periodicSingularSeries_periodic line 44