OAI/NumberTheory/Ostmann/QuadraticCenter/ParameterPrimeBand.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.logarithmicPrimeBand line 12
2. lemma OAI.Ostmann.QuadraticCenter.mem_logarithmicPrimeBand line 15
3. lemma OAI.Ostmann.QuadraticCenter.primeWeight_prime_interval_lower line 40
4. lemma OAI.Ostmann.QuadraticCenter.logarithmicPrimeBand_weight_lower line 53
5. def OAI.Ostmann.QuadraticCenter.boundedLogarithmicPrimeBand line 65
6. lemma OAI.Ostmann.QuadraticCenter.boundedLogarithmicPrimeBand_image line 68
7. lemma OAI.Ostmann.QuadraticCenter.boundedLogarithmicPrimeBand_weight_lower line 82