OAI/NumberTheory/JointDickman/Amplification/AmplificationDyadicIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact reconstruction of the unpartitioned amplification triple sum

  1. def OAI.JointDickman.amplificationArithmeticSum line 11
  2. theorem OAI.JointDickman.sum_triple_interchange line 16
  3. theorem OAI.JointDickman.amplification_dyadic_identity line 28