OAI/NumberTheory/JointDickman/Amplification/AmplificationRegularityIdentity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact dyadic recombination of the discarded regularity mass

  1. def OAI.JointDickman.discardedAmplificationTerm line 12
  2. def OAI.JointDickman.discardedAmplificationBoxTerm line 18
  3. theorem OAI.JointDickman.discardedAmplificationBoxTerm_eq line 24
  4. theorem OAI.JointDickman.discardedAmplificationBoxTerm_support line 36
  5. theorem OAI.JointDickman.discardedAmplificationBox_sum line 47
  6. theorem OAI.JointDickman.discarded_amplification_dyadic_identity line 87