OAI/NumberTheory/Ostmann/Preliminaries/SummandTails.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Actual finite tails of the two summands

  1. def OAI.Ostmann.summandPrefix line 15
  2. def OAI.Ostmann.summandTail line 18
  3. def OAI.Ostmann.positiveSummandTail line 21
  4. def OAI.Ostmann.negativeSummandTail line 24
  5. theorem OAI.Ostmann.mem_summandPrefix line 27
  6. theorem OAI.Ostmann.mem_summandTail line 32
  7. theorem OAI.Ostmann.summandPrefix_card_split line 37
  8. theorem OAI.Ostmann.positiveSummandTail_card line 55
  9. theorem OAI.Ostmann.negativeSummandTail_card line 62
  10. theorem OAI.Ostmann.positiveSummandTail_bounds line 68
  11. theorem OAI.Ostmann.negativeSummandTail_bounds line 74
  12. theorem OAI.Ostmann.EventuallyPrimeSumset.tail_prime_differences line 80