OAI/NumberTheory/PrimePackets/PenaltyEuler.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.Sieve.smallPrimes line 32
2. def OAI.PrimeDegreePackets.Sieve.penaltyEuler line 34
3. lemma OAI.PrimeDegreePackets.Sieve.penaltyEuler_one_le line 37
4. lemma OAI.PrimeDegreePackets.Sieve.penaltyEuler_mono line 45
5. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_le_softWeight line 57
6. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_interval_bound line 77
7. lemma OAI.PrimeDegreePackets.Sieve.interval_div_length_le line 93
8. lemma OAI.PrimeDegreePackets.Sieve.sum_le_mul_sum_reciprocal line 103
9. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_pow_reciprocal_le line 116
10. theorem OAI.PrimeDegreePackets.Sieve.sum_primePenalty_largeFactor_bound line 126
11. lemma OAI.PrimeDegreePackets.Sieve.sum_primePenalty_largeFactor_bound' line 182
12. theorem OAI.PrimeDegreePackets.Sieve.primePenalty_pow_interval_finite line 205
13. lemma OAI.PrimeDegreePackets.Sieve.sieve_error_scaled line 275
14. lemma OAI.PrimeDegreePackets.Sieve.primePenalty_pow_interval_at_level line 314
15. theorem OAI.PrimeDegreePackets.Sieve.primePenalty_pow_interval_uniform line 401
16. lemma OAI.PrimeDegreePackets.Sieve.reciprocal_gap_sum line 429
17. lemma OAI.PrimeDegreePackets.Sieve.prime_reciprocal_gap_le_one line 439
18. lemma OAI.PrimeDegreePackets.Sieve.penaltyEuler_le_exp line 459
19. lemma OAI.PrimeDegreePackets.Sieve.penaltyEuler_pow_le_exp line 487
20. theorem OAI.PrimeDegreePackets.Sieve.primePenalty_pow_relative_interval line 503