OAI/NumberTheory/Jacobsthal/Renewal/RegenerationDrift.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.RegenerationTails.tailDensity_setIntegral line 18
  2. theorem OAI.Erdos970.NumberTheoryLean.RegenerationTails.evenKernel_tail line 27
  3. theorem OAI.Erdos970.NumberTheoryLean.RegenerationTails.oddKernel_tail line 38
  4. theorem OAI.Erdos970.NumberTheoryLean.RegenerationTails.exponential_comparison line 51
  5. theorem OAI.Erdos970.NumberTheoryLean.RegenerationTails.kernel_exponential_tails line 87
  6. def OAI.Erdos970.NumberTheoryLean.RegenerationTails.regenerationState line 112
  7. theorem OAI.Erdos970.NumberTheoryLean.RegenerationTails.oddKernel_regeneration line 114
  8. theorem OAI.Erdos970.NumberTheoryLean.RegenerationTails.stateKernel_regeneration line 125
  9. theorem OAI.Erdos970.NumberTheoryLean.RegenerationTails.costKernel_regeneration line 131
  10. theorem OAI.Erdos970.NumberTheoryLean.RegenerationDrift.exponential_moment_of_tail line 150
  11. theorem OAI.Erdos970.NumberTheoryLean.RegenerationDrift.exponential_integrable_of_tail line 207
  12. def OAI.Erdos970.NumberTheoryLean.RegenerationDrift.driftFactor line 215
  13. theorem OAI.Erdos970.NumberTheoryLean.RegenerationDrift.driftFactor_pos line 217
  14. theorem OAI.Erdos970.NumberTheoryLean.RegenerationDrift.driftFactor_lt_one line 218
  15. theorem OAI.Erdos970.NumberTheoryLean.RegenerationDrift.drift_scale line 222
  16. theorem OAI.Erdos970.NumberTheoryLean.RegenerationDrift.kernel_exponential_drift line 227
  17. theorem OAI.Erdos970.NumberTheoryLean.RegenerationDrift.kernel_drift_expectation line 244