OAI/NumberTheory/JointDickman/Counting/CountingRamp.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A continuous approximation of the actual counting-scale cutoff

  1. def OAI.JointDickman.countingRamp line 11
  2. theorem OAI.JointDickman.countingRamp_bounds line 13
  3. theorem OAI.JointDickman.countingRamp_zero line 17
  4. theorem OAI.JointDickman.countingRamp_one line 20
  5. theorem OAI.JointDickman.countingRamp_continuous line 23
  6. theorem OAI.JointDickman.countingRamp_sharp_error line 34
  7. theorem OAI.JointDickman.finiteCandidateCutoff_threshold line 51
  8. def OAI.JointDickman.countingBand line 80
  9. theorem OAI.JointDickman.countingBand_bounds line 83
  10. theorem OAI.JointDickman.countingBand_continuous line 92
  11. theorem OAI.JointDickman.countingRamp_error_le_band line 103
  12. theorem OAI.JointDickman.countingBand_zero line 117