OAI/NumberTheory/Jacobsthal/Renewal/DickmanFiniteDecay.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.DelayConstruction.kernel line 21

    Also declared: ComparatorChallenges/JointDickman.lean:9 (same declaration text).

  2. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.kernel_continuous line 23
  3. def OAI.Erdos970.NumberTheoryLean.DelayConstruction.stepApprox line 30

    Also declared: ComparatorChallenges/JointDickman.lean:11 (same declaration text).

  4. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.stepApprox_continuous line 34
  5. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.stepApprox_initial line 43
  6. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.stepApprox_succ_stable line 46
  7. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.stepApprox_stable line 67
  8. def OAI.Erdos970.NumberTheoryLean.DelayConstruction.delay line 76

    Also declared: ComparatorChallenges/JointDickman.lean:15 (same declaration text).

  9. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.delay_eq_stepApprox line 78
  10. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.delay_continuous line 86
  11. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.delay_initial line 96
  12. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.delay_integral line 100
  13. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.delay_integral_of_one_le line 115
  14. theorem OAI.Erdos970.NumberTheoryLean.DelayConstruction.delay_hasDerivAt line 124
  15. theorem OAI.Erdos970.NumberTheoryLean.DelayUniqueness.shifted_unique_upto line 144
  16. theorem OAI.Erdos970.NumberTheoryLean.DelayUniqueness.shifted_unique line 168
  17. def OAI.Erdos970.NumberTheoryLean.Dickman.rho line 189

    Also declared: ComparatorChallenges/JointDickman.lean:22 (same declaration text).

  18. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_continuous line 191
  19. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_initial line 193
  20. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_hasDerivAt line 195
  21. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_delay_equation line 199
  22. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_integral line 203
  23. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_first_interval line 207
  24. def OAI.Erdos970.NumberTheoryLean.Dickman.primitive line 217
  25. theorem OAI.Erdos970.NumberTheoryLean.Dickman.primitive_continuous line 219
  26. theorem OAI.Erdos970.NumberTheoryLean.Dickman.primitive_hasDerivAt line 222
  27. def OAI.Erdos970.NumberTheoryLean.Dickman.identityDifference line 226
  28. theorem OAI.Erdos970.NumberTheoryLean.Dickman.identityDifference_continuous line 228
  29. theorem OAI.Erdos970.NumberTheoryLean.Dickman.identityDifference_hasDerivAt line 232
  30. theorem OAI.Erdos970.NumberTheoryLean.Dickman.identityDifference_one line 244
  31. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_unit_integral line 257
  32. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_antitone_segment line 271
  33. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_nonneg_upto line 283
  34. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_nonneg line 312
  35. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_antitone line 319
  36. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_half_step line 331
  37. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_lower_comparison line 349
  38. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_pos_initial line 361
  39. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_pos_upto line 372
  40. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_pos line 387
  41. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_upper_comparison line 392
  42. theorem OAI.Erdos970.NumberTheoryLean.Dickman.rho_ratio_bounds line 401
  43. def OAI.Erdos970.NumberTheoryLean.DickmanDecay.hazard line 425
  44. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.hazard_eq_neg_deriv line 427
  45. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.hazard_ge_one line 432
  46. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.deriv_le_of_hazard line 437
  47. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.rho_exponential_comparison line 443
  48. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.unit_exponential_integral line 480
  49. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.hazard_bootstrap line 489
  50. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.bootstrap_uniform_gain line 510
  51. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.hazard_step_bound line 520
  52. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.exists_hazard_tail line 552
  53. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.negative_logDeriv_tail line 568
  54. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.hazard_tendsto_atTop line 576
  55. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.rho_exponential_majorant line 582
  56. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.rho_faster_than_exponential line 596
  57. theorem OAI.Erdos970.NumberTheoryLean.DickmanDecay.rho_tendsto_zero line 617
  58. theorem OAI.Erdos970.NumberTheoryLean.DickmanFiniteDecay.rho_le_one line 630
  59. theorem OAI.Erdos970.NumberTheoryLean.DickmanFiniteDecay.rho_step_power line 636
  60. theorem OAI.Erdos970.NumberTheoryLean.DickmanFiniteDecay.rho_half_power line 653
  61. theorem OAI.Erdos970.NumberTheoryLean.DickmanFiniteDecay.rho_log_decay line 664