OAI/NumberTheory/JointDickman/Arithmetic/DivisorProductMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite divisor expansion and its mean bound

  1. theorem OAI.JointDickman.primeProduct_dvd_iff line 13

    Distinct definitions of this name: OAI/NumberTheory/JointDickman/Analysis/MellinSieveRemainder.lean:12 (different declaration text), OAI/NumberTheory/JointDickman/Arithmetic/SmoothInclusionExclusion.lean:25 (different declaration text). Qualify references as OAI.JointDickman.primeProduct_dvd_iff@path.

  2. theorem OAI.JointDickman.divisor_product_expansion line 23
  3. theorem OAI.JointDickman.divisor_product_mean line 37