OAI/NumberTheory/JointDickman/Arithmetic/SquarefreeSingularFactor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The analytic factor determining the Selberg–Delange coefficients

  1. def OAI.JointDickman.squarefreeSingularFactor line 11

    Source documentation

    Removing the principal power singularity of ζ(s)^z and the Perron denominator.

    noncomputable def squarefreeSingularFactor (z : ℝ) (s : ℂ) : ℂ :=
…
  2. theorem OAI.JointDickman.squarefreeSingularFactor_analyticAt_one line 14
  3. theorem OAI.JointDickman.squarefreeSingularFactor_one line 21
  4. theorem OAI.JointDickman.squarefreeSingularFactor_hasPowerSeries line 26