OAI/NumberTheory/JointDickman/Arithmetic/RamanujanDivisorFormula.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An exact divisor formula for all Ramanujan frequencies

  1. def OAI.JointDickman.ramanujanSum line 11
  2. theorem OAI.JointDickman.ramanujanSum_zero line 14
  3. theorem OAI.JointDickman.ramanujanSum_unit line 18
  4. theorem OAI.JointDickman.sum_nthRoots_power line 21
  5. theorem OAI.JointDickman.sum_primitiveRoots_power line 34

    Source documentation

    Möbius inversion of the full root sums. This includes nonunit frequencies.

    theorem sum_primitiveRoots_power (q : ℕ) (hq : 0 < q) (k : ℕ) :
    (∑ z ∈ primitiveRoots q ℂ, z^k) =
      ∑ d ∈ q.divisorsAntidiagonal, (μ d.1 : ℂ)*
        (if d.2 ∣ k then (d.2 : ℂ) else 0) := by
…
  6. theorem OAI.JointDickman.ramanujanSum_divisor_formula line 46