OAI/NumberTheory/SiegelZeros/Structure/CharacterEstimates.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.WeightedTorusJets.combined_vonMangoldt_LSeries line 24
2. theorem OAI.SiegelZeros.WeightedTorusJets.combined_vonMangoldt_summable line 41
3. theorem OAI.SiegelZeros.WeightedTorusJets.re_combined_vonMangoldt_term line 49
4. theorem OAI.SiegelZeros.WeightedTorusJets.combined_vonMangoldt_term_nonneg line 63
5. theorem OAI.SiegelZeros.WeightedTorusJets.prime_sum_rpow_le_logDeriv line 77
6. theorem OAI.SiegelZeros.WeightedTorusJets.log_rpow_compare line 106
7. theorem OAI.SiegelZeros.WeightedTorusJets.positive_prime_mass_le_logDeriv_floor line 125
8. theorem OAI.SiegelZeros.WeightedTorusJets.reciprocal_gap_identity line 153
9. theorem OAI.SiegelZeros.WeightedTorusJets.reciprocal_gap_le line 160
10. theorem OAI.SiegelZeros.WeightedTorusJets.primebias_sampling_point line 172
11. theorem OAI.SiegelZeros.WeightedTorusJets.positive_prime_mass_of_logDeriv_upper line 183
12. theorem OAI.SiegelZeros.RealCharacterAnalysis.real_values_iff_quadratic line 214
13. theorem OAI.SiegelZeros.RealCharacterAnalysis.apply_prime_eq_zero_iff line 231
14. theorem OAI.SiegelZeros.RealCharacterAnalysis.lSeries_conj line 235
15. theorem OAI.SiegelZeros.RealCharacterAnalysis.lFunction_conj line 246
16. theorem OAI.SiegelZeros.RealCharacterAnalysis.lFunction_real line 274
17. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.sum_log_le line 298
18. lemma OAI.SiegelZeros.WeightedTorusJets.Mertens.integral_log_le line 311
19. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.sum_log_ge line 322
20. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.sum_log_eq_sum_mangoldt line 351
21. abbrev OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁Λ line 356
22. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁Λ.ge line 358
23. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁Λ.le line 374
24. abbrev OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁p line 395
25. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁p.le_E₁Λ line 397
26. abbrev OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁ line 406
27. lemma OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁.summand_nonneg line 408
28. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁.summable line 415
29. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁.nonneg line 439
30. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.E₁Λ.le_E₁p_add_E₁ line 442
31. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.prime_log_div_bounded_error line 485
32. theorem OAI.SiegelZeros.WeightedTorusJets.Mertens.prime_log_div_isBigO line 496