OAI/NumberTheory/JointDickman/Arithmetic/SmoothArithmeticTensor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite tensor expansion of the full smooth arithmetic weight

  1. def OAI.JointDickman.geometricSmoothArithmeticSum line 11
  2. theorem OAI.JointDickman.geometricSmoothArithmeticSum_separated line 26
  3. theorem OAI.JointDickman.geometricSmoothArithmeticSum_sum line 44
  4. theorem OAI.JointDickman.geometricSmoothArithmeticSum_tensor line 68