OAI/NumberTheory/Ostmann/Supply/TailSieveEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The sieve budget on the two actual summand tails

  1. theorem OAI.Ostmann.tail_sieve_energy_budgets line 10
  2. theorem OAI.Ostmann.summandTail_pair_sum line 69