OAI/NumberTheory/Jacobsthal/Estimates/SourceParentBenchmark.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosSourceReferenceMargin.starting_extension_derivative_two line 20
  2. theorem OAI.Erdos970.ErdosSourceReferenceMargin.starting_extension_two line 27
  3. def OAI.Erdos970.ErdosSourceReferenceMargin.startingSlope line 29
  4. theorem OAI.Erdos970.ErdosSourceReferenceMargin.startingSlope_continuousAt line 33
  5. theorem OAI.Erdos970.ErdosSourceReferenceMargin.startingSlope_two line 36
  6. theorem OAI.Erdos970.ErdosSourceReferenceMargin.starting_extension_factor line 38
  7. theorem OAI.Erdos970.ErdosSourceReferenceMargin.root_startingSlope_tendsto line 45
  8. theorem OAI.Erdos970.ErdosSourceReferenceMargin.root_parentBenchmark_tendsto line 50
  9. theorem OAI.Erdos970.ErdosSourceReferenceMargin.root_nodeBenchmark_tendsto line 64