OAI/NumberTheory/Jacobsthal/Siegel/MellinConvergentTopIndicator.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Erdos970.WeightedTorusJets.mellinConvergent_top_indicator line 24
  2. lemma OAI.Erdos970.WeightedTorusJets.f_modif_eq_top_add_inv line 36
  3. lemma OAI.Erdos970.WeightedTorusJets.mellin_top_indicator_eq line 55
  4. lemma OAI.Erdos970.WeightedTorusJets.Lambda_zero_eq_top_integrals line 61
  5. lemma OAI.Erdos970.WeightedTorusJets.norm_top_integral_le line 92
  6. theorem OAI.Erdos970.WeightedTorusJets.norm_Lambda_zero_le_top_integrals line 102
  7. theorem OAI.Erdos970.WeightedTorusJets.exponential_moment_integrable line 118
  8. theorem OAI.Erdos970.WeightedTorusJets.exponential_moment_pointwise line 125
  9. theorem OAI.Erdos970.WeightedTorusJets.exponential_moment_le line 143
  10. theorem OAI.Erdos970.WeightedTorusJets.mul_log_le_three_halves line 167
  11. theorem OAI.Erdos970.WeightedTorusJets.exponential_moment_growth line 178
  12. theorem OAI.Erdos970.WeightedTorusJets.log_one_add_le_log_two_add line 206
  13. theorem OAI.Erdos970.WeightedTorusJets.log_norm_growth_of_norm_growth line 213
  14. lemma OAI.Erdos970.WeightedTorusJets.weighted_norm_integral_le_moment line 236
  15. theorem OAI.Erdos970.WeightedTorusJets.norm_Lambda_zero_growth_of_exp_bounds line 253
  16. theorem OAI.Erdos970.WeightedTorusJets.exists_global_exp_bound line 330
  17. theorem OAI.Erdos970.WeightedTorusJets.exists_evenKernel_sub_exp_bound line 360
  18. theorem OAI.Erdos970.WeightedTorusJets.exists_cosKernel_sub_exp_bound line 369
  19. theorem OAI.Erdos970.WeightedTorusJets.exists_oddKernel_exp_bound line 377
  20. theorem OAI.Erdos970.WeightedTorusJets.exists_sinKernel_exp_bound line 385
  21. theorem OAI.Erdos970.WeightedTorusJets.exists_hurwitzEvenFEPair_f_exp_bound line 393
  22. theorem OAI.Erdos970.WeightedTorusJets.exists_hurwitzEvenFEPair_g_exp_bound line 403
  23. theorem OAI.Erdos970.WeightedTorusJets.exists_hurwitzOddFEPair_f_exp_bound line 412
  24. theorem OAI.Erdos970.WeightedTorusJets.exists_hurwitzOddFEPair_g_exp_bound line 420
  25. theorem OAI.Erdos970.WeightedTorusJets.norm_growth_half_shift line 430
  26. theorem OAI.Erdos970.WeightedTorusJets.norm_completedHurwitzZetaEven_zero_growth_of_Lambda_zero_growth line 464
  27. theorem OAI.Erdos970.WeightedTorusJets.norm_completedHurwitzZetaOdd_growth_of_Lambda_zero_growth line 475
  28. theorem OAI.Erdos970.WeightedTorusJets.exists_completedHurwitzZetaEven_zero_growth line 492
  29. theorem OAI.Erdos970.WeightedTorusJets.exists_completedHurwitzZetaOdd_growth line 500