OAI/NumberTheory/Jacobsthal/Primes/PrimePowerBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosKloosterman.PrimePower.envelope line 12
2. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.envelope_ge_primitive line 16
3. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.quarter_scale line 31
4. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.envelope_scale line 43
5. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.prime_zero_envelope line 67
6. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.prime_envelope_bound line 81
7. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.prime_power_envelope_bound line 109
8. theorem OAI.Erdos970.ErdosKloosterman.PrimePower.standardSum_prime_power_bound line 133