OAI/NumberTheory/Jacobsthal/Estimates/OmissionSeries.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosContinuousOmission.baseCutoff line 14
  2. def OAI.Erdos970.ErdosContinuousOmission.survivorBaseline line 15
  3. theorem OAI.Erdos970.ErdosContinuousOmission.baseCutoff_bounds line 17
  4. theorem OAI.Erdos970.ErdosContinuousOmission.baseCutoff_on line 20
  5. theorem OAI.Erdos970.ErdosContinuousOmission.cutoff_le_base line 23
  6. theorem OAI.Erdos970.ErdosContinuousOmission.survivorBaseline_continuous line 28
  7. theorem OAI.Erdos970.ErdosContinuousOmission.baseline_profile_continuous line 32
  8. theorem OAI.Erdos970.ErdosContinuousOmission.gate_survivorBaseline line 35
  9. def OAI.Erdos970.ErdosContinuousOmission.omissionForce line 61
  10. theorem OAI.Erdos970.ErdosContinuousOmission.omissionForce_continuous line 65
  11. theorem OAI.Erdos970.ErdosContinuousOmission.omissionForce_nonnegative line 74
  12. def OAI.Erdos970.ErdosContinuousOmission.omissionDefect line 93
  13. theorem OAI.Erdos970.ErdosContinuousOmission.omissionDefect_continuous line 97
  14. theorem OAI.Erdos970.ErdosContinuousOmission.gate_sub line 103
  15. theorem OAI.Erdos970.ErdosContinuousOmission.gate_defect_even line 110
  16. theorem OAI.Erdos970.ErdosContinuousOmission.gate_defect_odd line 115
  17. theorem OAI.Erdos970.ErdosContinuousOmission.actual_defect_forcing line 120
  18. theorem OAI.Erdos970.ErdosContinuousOmission.actual_finite_omission_expansion line 134
  19. theorem OAI.Erdos970.ErdosContinuousOmission.omissionDefect_nonnegative line 141
  20. theorem OAI.Erdos970.ErdosContinuousOmission.actual_reference_order line 147
  21. theorem OAI.Erdos970.ErdosContinuousOmission.partial_omission_le_defect line 154
  22. theorem OAI.Erdos970.ErdosContinuousOmission.omission_terms_vanish line 171
  23. theorem OAI.Erdos970.ErdosContinuousOmission.actual_omission_hasSum line 178
  24. theorem OAI.Erdos970.ErdosContinuousOmission.actual_omission_tsum line 186
  25. theorem OAI.Erdos970.ErdosContinuousOmission.actual_omission_summable line 190