OAI/NumberTheory/Ostmann/Preliminaries/SummandPolynomialBootstrap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A concrete polynomial bootstrap for summand counts

The second sampling length is exponential. Only the integer powers 6, 8 and 12 are needed; a general subpower theorem is unnecessary for this application.

  1. theorem OAI.Ostmann.constant_log_linear_small line 16
  2. theorem OAI.Ostmann.EventuallyPrimeSumset.summand_polynomial_bootstrap line 31