OAI/NumberTheory/Jacobsthal/Siegel/E.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.combined_vonMangoldt_LSeries line 26
  2. theorem OAI.Erdos970.WeightedTorusJets.combined_vonMangoldt_summable line 43
  3. theorem OAI.Erdos970.WeightedTorusJets.re_combined_vonMangoldt_term line 51
  4. theorem OAI.Erdos970.WeightedTorusJets.combined_vonMangoldt_term_nonneg line 65
  5. theorem OAI.Erdos970.WeightedTorusJets.prime_sum_rpow_le_logDeriv line 79
  6. theorem OAI.Erdos970.WeightedTorusJets.log_rpow_compare line 108
  7. theorem OAI.Erdos970.WeightedTorusJets.positive_prime_mass_le_logDeriv_floor line 127
  8. theorem OAI.Erdos970.WeightedTorusJets.reciprocal_gap_identity line 159
  9. theorem OAI.Erdos970.WeightedTorusJets.reciprocal_gap_le line 166
  10. theorem OAI.Erdos970.WeightedTorusJets.primebias_sampling_point line 178
  11. theorem OAI.Erdos970.WeightedTorusJets.positive_prime_mass_of_logDeriv_upper line 194
  12. theorem OAI.Erdos970.RealCharacterAnalysis.real_values_iff_quadratic line 228
  13. theorem OAI.Erdos970.RealCharacterAnalysis.apply_prime_eq_zero_iff line 245
  14. theorem OAI.Erdos970.RealCharacterAnalysis.lSeries_conj line 249
  15. theorem OAI.Erdos970.RealCharacterAnalysis.lFunction_conj line 260
  16. theorem OAI.Erdos970.RealCharacterAnalysis.lFunction_real line 288
  17. theorem OAI.Erdos970.WeightedTorusJets.Mertens.sum_log_le line 314
  18. lemma OAI.Erdos970.WeightedTorusJets.Mertens.integral_log_le line 327
  19. theorem OAI.Erdos970.WeightedTorusJets.Mertens.sum_log_ge line 338
  20. theorem OAI.Erdos970.WeightedTorusJets.Mertens.sum_log_eq_sum_mangoldt line 367
  21. abbrev OAI.Erdos970.WeightedTorusJets.Mertens.E₁Λ line 372
  22. theorem OAI.Erdos970.WeightedTorusJets.Mertens.E₁Λ.ge line 374
  23. theorem OAI.Erdos970.WeightedTorusJets.Mertens.E₁Λ.le line 390
  24. abbrev OAI.Erdos970.WeightedTorusJets.Mertens.E₁p line 411
  25. theorem OAI.Erdos970.WeightedTorusJets.Mertens.E₁p.le_E₁Λ line 413
  26. abbrev OAI.Erdos970.WeightedTorusJets.Mertens.E₁ line 422
  27. lemma OAI.Erdos970.WeightedTorusJets.Mertens.E₁.summand_nonneg line 424
  28. theorem OAI.Erdos970.WeightedTorusJets.Mertens.E₁.summable line 431
  29. theorem OAI.Erdos970.WeightedTorusJets.Mertens.E₁.nonneg line 455
  30. theorem OAI.Erdos970.WeightedTorusJets.Mertens.E₁Λ.le_E₁p_add_E₁ line 458
  31. theorem OAI.Erdos970.WeightedTorusJets.Mertens.prime_log_div_bounded_error line 501
  32. theorem OAI.Erdos970.WeightedTorusJets.Mertens.prime_log_div_isBigO line 512