OAI/NumberTheory/Jacobsthal/Primes/WeightedPrimeMultiplePairs.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.primeMultiplesIn line 14
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.mem_primeMultiplesIn line 19
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_multiple_pos_injective line 30
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_multiple_neg_injective line 37
5. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.signed_prime_sets_card_le line 42
6. theorem OAI.Erdos970.ErdosStoppedArithmetic.large_prime_factor_unique line 87
7. theorem OAI.Erdos970.ErdosStoppedArithmetic.prime_multiple_natAbs line 101
8. theorem OAI.Erdos970.ErdosStoppedArithmetic.prime_multiple_factors_disjoint line 108
9. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_multiple_d_le_P line 124
10. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_multiple_P_sq_le line 130
11. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_multiple_interval_height line 135
12. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_multiple_piece_bounds line 143
13. def OAI.Erdos970.ErdosStoppedArithmetic.admissiblePairs line 225
14. theorem OAI.Erdos970.ErdosStoppedArithmetic.admissible_pair_card_rows line 228
15. theorem OAI.Erdos970.ErdosStoppedArithmetic.admissible_pair_card_columns line 232
16. theorem OAI.Erdos970.ErdosStoppedArithmetic.prime_multiple_pair_sum line 238
17. theorem OAI.Erdos970.ErdosStoppedArithmetic.prime_multiple_pair_lower line 247
18. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_multiple_height_eventually line 278
19. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.prime_multiple_endpoint_loss line 321
20. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.retainedPrimes line 360
21. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.mem_retainedPrimes line 363
22. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.retained_positive_data line 370
23. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.retained_negative_data line 384
24. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.retained_count_lower line 407
25. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.moving_signed_prime_multiple_lower line 430
26. theorem OAI.Erdos970.ErdosStoppedArithmetic.supported_small_factor_bounds line 547
27. theorem OAI.Erdos970.ErdosStoppedArithmetic.paper_weight_nonneg line 556
28. theorem OAI.Erdos970.ErdosStoppedArithmetic.moving_weighted_pair_lower line 567