OAI/NumberTheory/JointDickman/Amplification/GeometricDyadicPartition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact dyadic recombination of the original amplification weight

  1. def OAI.JointDickman.dyadicBoxIndices line 10
  2. theorem OAI.JointDickman.exp_nat_log_two line 13
  3. theorem OAI.JointDickman.geometric_dyadic_partition line 16
  4. theorem OAI.JointDickman.amplificationBoxWeight_normalized line 25
  5. theorem OAI.JointDickman.amplificationBoxWeight_dyadic_sum line 39