OAI/NumberTheory/Ostmann/Construction/TailBandCollision.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The collision budget on the band used in Proposition 5.1

  1. theorem OAI.Ostmann.eventual_logLogPrimeBand_subset_collision_cutoff line 10
  2. theorem OAI.Ostmann.EventuallyPrimeSumset.tail_band_collision_budget line 35