OAI/NumberTheory/JointDickman/Counting/ShortLagSet.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The singular factor has bounded mean on both signs of the short lags

  1. def OAI.JointDickman.nonzeroShortLags line 10
  2. theorem OAI.JointDickman.mem_nonzeroShortLags line 12
  3. theorem OAI.JointDickman.nonzeroShortLags_eq line 25
  4. theorem OAI.JointDickman.sum_shortLag_natAbs line 46
  5. theorem OAI.JointDickman.shortLag_singular_sum line 66