OAI/NumberTheory/Jacobsthal/Siegel/SumLogPrimeFactors.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.WeightedTorusJets.sum_log_primeFactors_le line 20
2. theorem OAI.Erdos970.WeightedTorusJets.sum_log_div_primeFactors_le line 32
3. theorem OAI.Erdos970.WeightedTorusJets.sum_log_div_filter_dvd_le line 39
4. theorem OAI.Erdos970.WeightedTorusJets.sum_log_div_filter_le_cutoff line 50
5. theorem OAI.Erdos970.WeightedTorusJets.prime_mass_partition_le line 67
6. theorem OAI.Erdos970.WeightedTorusJets.good_mass_of_estimates line 103
7. theorem OAI.Erdos970.WeightedTorusJets.good_prime_mass_of_primebias line 122
8. theorem OAI.Erdos970.WeightedTorusJets.source_analytic_lemma line 165
9. theorem OAI.Erdos970.WeightedTorusJets.source_hadamard_logDeriv_identity line 241
10. theorem OAI.Erdos970.WeightedTorusJets.source_logDeriv_upper line 258
11. theorem OAI.Erdos970.WeightedTorusJets.logDeriv_real_of_complex line 278
12. theorem OAI.Erdos970.WeightedTorusJets.source_hadamard_logDeriv_identity_real line 291
13. theorem OAI.Erdos970.WeightedTorusJets.completedL_analyticOrderAt_eq_LFunction line 317
14. theorem OAI.Erdos970.WeightedTorusJets.conductorCompletedL_analyticOrderAt_eq_LFunction line 345
15. theorem OAI.Erdos970.WeightedTorusJets.exists_radius_LFunction_ne_zero line 354
16. theorem OAI.Erdos970.WeightedTorusJets.exists_radius_LFunction_ne_zero_fixed_modulus line 367
17. theorem OAI.Erdos970.WeightedTorusJets.exists_gap_fixed_modulus line 386
18. theorem OAI.Erdos970.WeightedTorusJets.exists_gap_bounded_moduli line 399
19. theorem OAI.Erdos970.WeightedTorusJets.exists_small_gap_large_modulus line 422
20. theorem OAI.Erdos970.WeightedTorusJets.exists_contrary_sequence line 451