OAI/NumberTheory/JointDickman/Amplification/OccupiedRootComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cost of setting auxiliary root tests to zero at occupied primes

  1. theorem OAI.JointDickman.bernoulli_l1_empty line 12
  2. def OAI.JointDickman.siteConditionedRootPrimeMass line 33
  3. theorem OAI.JointDickman.siteConditionedRootPrimeMass_nonneg line 39
  4. theorem OAI.JointDickman.siteConditionedRootPrimeMass_sum line 46
  5. theorem OAI.JointDickman.siteConditionedRootPrimeMass_l1 line 59