OAI/NumberTheory/JointDickman/Amplification/OutsideCandidateMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Conditional candidate-root distribution at an unoccupied prime

  1. def OAI.JointDickman.outsideCandidatePrimeMass line 11
  2. theorem OAI.JointDickman.blockForbidden_card line 15
  3. theorem OAI.JointDickman.outsideCandidatePrimeMass_nonneg line 20
  4. theorem OAI.JointDickman.outsideCandidatePrimeMass_sum line 24
  5. theorem OAI.JointDickman.outsideCandidatePrimeMass_l1 line 31