OAI/NumberTheory/JointDickman/Analysis/SquarefreeDirichletSeries.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The squarefree Dirichlet series and its Euler product

These identities begin the analytic discharge of the two fixed-exponent Selberg–Delange expansions. They do not assume an asymptotic for the coefficients.

  1. theorem OAI.JointDickman.squarefreeLeadingConstant_pos line 15
  2. theorem OAI.JointDickman.squarefreeWeight_abs_le_one line 23

    Distinct definitions of this name: OAI/NumberTheory/JointDickman/Counting/ConvolutionTail.lean:17 (same statement text; different proof or body). Qualify references as OAI.JointDickman.squarefreeWeight_abs_le_one@path.

  3. def OAI.JointDickman.squarefreeDirichletSummand line 31
  4. theorem OAI.JointDickman.squarefreeDirichletSummand_term line 34
  5. theorem OAI.JointDickman.squarefreeDirichletSummand_zero line 39
  6. theorem OAI.JointDickman.squarefreeDirichletSummand_one line 42
  7. theorem OAI.JointDickman.squarefreeDirichletSummand_mul line 45
  8. theorem OAI.JointDickman.squarefreeDirichletSummand_summable line 55
  9. theorem OAI.JointDickman.squarefreeDirichletSummand_prime_tsum line 62
  10. theorem OAI.JointDickman.squarefreeDirichletSeries_eulerProduct line 73