OAI/NumberTheory/JointDickman/UnconditionalMain.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The joint Dickman law and both strict ordering densities

The joint distribution follows from character-distance divergence, upper sieves, Selberg–Delange estimates, concentration, and finite-bin Dickman distributions.

  1. theorem OAI.JointDickman.rationalFixedScaleLaw_unconditional line 14
  2. theorem OAI.JointDickman.jointDickmanLaw_unconditional line 20
  3. theorem OAI.JointDickman.increasingOrderLaw_unconditional line 23
  4. theorem OAI.JointDickman.decreasingOrderLaw_unconditional line 26
  5. theorem OAI.JointDickman.main_results_unconditional line 29