OAI/NumberTheory/Ostmann/QuadraticCenter/QuadraticBiasLittleO.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.eventually_quadraticBadBandMass_le line 16
2. def OAI.Ostmann.QuadraticCenter.quadraticLogBandMass line 29
3. lemma OAI.Ostmann.QuadraticCenter.quadraticLogBandMass_nonneg line 32
4. theorem OAI.Ostmann.QuadraticCenter.eventually_quadraticLogBandMass_le line 40
5. theorem OAI.Ostmann.QuadraticCenter.eventually_quadratic_prime_band_le line 51
6. theorem OAI.Ostmann.QuadraticCenter.quadraticLogBandMass_isLittleO line 65