OAI/NumberTheory/SiegelZeros/Characters/PrimePowerTail.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.W55.higherPrimePowerTerm line 15
2. lemma OAI.SiegelZeros.W55.higherPrimePowerTerm_nonneg line 18
3. theorem OAI.SiegelZeros.W55.summable_higherPrimePowerTerm line 22
4. def OAI.SiegelZeros.W55.higherPrimePowerConstant line 29
5. lemma OAI.SiegelZeros.W55.higherPrimePowerConstant_nonneg line 31
6. theorem OAI.SiegelZeros.W55.higherPrimePower_sum_le line 34
7. theorem OAI.SiegelZeros.W55.vonMangoldt_mass_split line 38
8. theorem OAI.SiegelZeros.W55.prime_mass_lower_of_vonMangoldt_mass_lower line 50