OAI/NumberTheory/JointDickman/Arithmetic/DickmanDistribution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The continuous Dickman distribution function

Continuity and endpoint behavior of the Dickman function determine its continuous distribution function and the limiting order probabilities.

  1. def OAI.JointDickman.dickmanCDF line 19
  2. theorem OAI.JointDickman.dickmanCDF_zero line 22
  3. theorem OAI.JointDickman.dickmanCDF_nonneg line 24
  4. theorem OAI.JointDickman.dickmanCDF_le_one line 30
  5. theorem OAI.JointDickman.dickmanCDF_eq_one line 36
  6. theorem OAI.JointDickman.dickmanCDF_monotone line 41
  7. theorem OAI.JointDickman.dickmanCDF_continuousAt_zero line 50
  8. theorem OAI.JointDickman.dickmanCDF_continuous line 67