OAI/NumberTheory/JointDickman/Arithmetic/SquarefreeLSeriesBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the original squarefree Dirichlet series on the right

  1. theorem OAI.JointDickman.squarefreeLSeries_norm line 11
  2. theorem OAI.JointDickman.squarefreeLSeries_high_bound line 18