OAI/NumberTheory/Jacobsthal/Estimates/GrowingFarTail.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.InverseWeightGrowth.quartic_log_scale_absorption line 14
  2. def OAI.Erdos970.NumberTheoryLean.ModerateFailedReward.moderateReward line 63
  3. theorem OAI.Erdos970.NumberTheoryLean.ModerateFailedReward.exponential_quartic_absorbs_linear line 68
  4. theorem OAI.Erdos970.NumberTheoryLean.ModerateFailedReward.moderate_reward_envelope line 76
  5. theorem OAI.Erdos970.NumberTheoryLean.ModerateFailedReward.actual_moderate_failed_sum line 107
  6. theorem OAI.Erdos970.NumberTheoryLean.SourceFarGapTail.source_far_gap_tail line 164
  7. def OAI.Erdos970.NumberTheoryLean.SourceModerateFailure.growingCutoff line 223
  8. theorem OAI.Erdos970.NumberTheoryLean.SourceModerateFailure.source_moderate_failure line 225
  9. theorem OAI.Erdos970.NumberTheoryLean.GrowingFarTail.growingCutoff_tendsto line 297
  10. theorem OAI.Erdos970.NumberTheoryLean.GrowingFarTail.log_cube_growing_exp_tendsto line 300
  11. def OAI.Erdos970.NumberTheoryLean.GrowingFarTail.farBudget line 312
  12. theorem OAI.Erdos970.NumberTheoryLean.GrowingFarTail.farBudget_tendsto_zero line 315
  13. theorem OAI.Erdos970.NumberTheoryLean.GrowingFarTail.source_horizon_comparison line 324
  14. theorem OAI.Erdos970.NumberTheoryLean.GrowingFarTail.source_growing_far_tail line 331