OAI/NumberTheory/Jacobsthal/Estimates/SourceCenteredGap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosCorrectionLimit.sourceRootGap line 17
  2. def OAI.Erdos970.ErdosCorrectionLimit.sourceRootNode line 20
  3. theorem OAI.Erdos970.ErdosCorrectionLimit.sourceRoot_eq_paper line 27
  4. theorem OAI.Erdos970.ErdosCorrectionLimit.floored_source_prefactor_tendsto line 36
  5. theorem OAI.Erdos970.ErdosCorrectionLimit.floored_source_correction_tendsto line 46
  6. theorem OAI.Erdos970.ErdosSourceReferenceMargin.log_sourceW_div_log_tendsto line 68
  7. theorem OAI.Erdos970.ErdosSourceReferenceMargin.log_div_log_sourceW_tendsto line 82
  8. theorem OAI.Erdos970.ErdosSourceReferenceMargin.centered_paper_gap_tendsto line 87
  9. theorem OAI.Erdos970.ErdosSourceReferenceMargin.rootW_tendsto line 97
  10. theorem OAI.Erdos970.ErdosSourceReferenceMargin.rootB_tendsto line 100
  11. theorem OAI.Erdos970.ErdosSourceReferenceMargin.actual_root_eventually line 103
  12. theorem OAI.Erdos970.ErdosSourceReferenceMargin.actual_root_ratio_tendsto line 113
  13. theorem OAI.Erdos970.ErdosSourceReferenceMargin.actual_root_centered_gap_tendsto line 121