OAI/NumberTheory/Ostmann/QuadraticCenter/AmplificationCountBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The precise number of small primes required for amplification

  1. theorem OAI.Ostmann.original_scale_power_quotient line 9
  2. theorem OAI.Ostmann.amplificationPrimeCount_bounds line 14