OAI/NumberTheory/Jacobsthal/Estimates/ReferenceCutoffRecurrence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.ReferenceWeightedRecurrence.weightedValue line 17
  2. theorem OAI.Erdos970.NumberTheoryLean.ReferenceWeightedRecurrence.weighted_reference_recurrence line 20
  3. theorem OAI.Erdos970.NumberTheoryLean.ReferenceForestTelescoping.suffixPrimes_nil line 63
  4. theorem OAI.Erdos970.NumberTheoryLean.ReferenceForestTelescoping.suffixPrimes_cons line 65
  5. def OAI.Erdos970.NumberTheoryLean.ReferenceForestTelescoping.forestSum line 70
  6. theorem OAI.Erdos970.NumberTheoryLean.ReferenceForestTelescoping.forestSum_recurrence line 73
  7. def OAI.Erdos970.NumberTheoryLean.ReferenceForestTelescoping.recurrenceResidual line 80
  8. theorem OAI.Erdos970.NumberTheoryLean.ReferenceForestTelescoping.actual_forest_telescoping line 84
  9. def OAI.Erdos970.NumberTheoryLean.ReferenceCutoffRecurrence.Above line 116
  10. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCutoffRecurrence.above_disjoint line 118
  11. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCutoffRecurrence.union_filter_at_high line 123
  12. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCutoffRecurrence.union_filter_at_low line 127
  13. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCutoffRecurrence.cutoff_polynomial_recurrence line 139
  14. def OAI.Erdos970.NumberTheoryLean.ReferenceCutoffRecurrence.cutoffInsertion line 163
  15. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCutoffRecurrence.difference_residual line 168
  16. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCutoffRecurrence.finite_cutoff_decomposition line 189