OAI/NumberTheory/SiegelZeros/EntireFunctions/MellinConvergentTopIndicator.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SiegelZeros.WeightedTorusJets.mellinConvergent_top_indicator line 19
  2. lemma OAI.SiegelZeros.WeightedTorusJets.f_modif_eq_top_add_inv line 31
  3. lemma OAI.SiegelZeros.WeightedTorusJets.mellin_top_indicator_eq line 50
  4. lemma OAI.SiegelZeros.WeightedTorusJets.Lambda_zero_eq_top_integrals line 56
  5. lemma OAI.SiegelZeros.WeightedTorusJets.norm_top_integral_le line 87
  6. theorem OAI.SiegelZeros.WeightedTorusJets.norm_Lambda_zero_le_top_integrals line 97
  7. theorem OAI.SiegelZeros.WeightedTorusJets.exponential_moment_integrable line 113
  8. theorem OAI.SiegelZeros.WeightedTorusJets.exponential_moment_pointwise line 120
  9. theorem OAI.SiegelZeros.WeightedTorusJets.exponential_moment_le line 138
  10. theorem OAI.SiegelZeros.WeightedTorusJets.mul_log_le_three_halves line 162
  11. theorem OAI.SiegelZeros.WeightedTorusJets.exponential_moment_growth line 173
  12. theorem OAI.SiegelZeros.WeightedTorusJets.log_one_add_le_log_two_add line 201
  13. theorem OAI.SiegelZeros.WeightedTorusJets.log_norm_growth_of_norm_growth line 208
  14. lemma OAI.SiegelZeros.WeightedTorusJets.weighted_norm_integral_le_moment line 229
  15. theorem OAI.SiegelZeros.WeightedTorusJets.norm_Lambda_zero_growth_of_exp_bounds line 246
  16. theorem OAI.SiegelZeros.WeightedTorusJets.exists_global_exp_bound line 323
  17. theorem OAI.SiegelZeros.WeightedTorusJets.exists_evenKernel_sub_exp_bound line 353
  18. theorem OAI.SiegelZeros.WeightedTorusJets.exists_cosKernel_sub_exp_bound line 362
  19. theorem OAI.SiegelZeros.WeightedTorusJets.exists_oddKernel_exp_bound line 370
  20. theorem OAI.SiegelZeros.WeightedTorusJets.exists_sinKernel_exp_bound line 378
  21. theorem OAI.SiegelZeros.WeightedTorusJets.exists_hurwitzEvenFEPair_f_exp_bound line 386
  22. theorem OAI.SiegelZeros.WeightedTorusJets.exists_hurwitzEvenFEPair_g_exp_bound line 396
  23. theorem OAI.SiegelZeros.WeightedTorusJets.exists_hurwitzOddFEPair_f_exp_bound line 405
  24. theorem OAI.SiegelZeros.WeightedTorusJets.exists_hurwitzOddFEPair_g_exp_bound line 413
  25. theorem OAI.SiegelZeros.WeightedTorusJets.norm_growth_half_shift line 421
  26. theorem OAI.SiegelZeros.WeightedTorusJets.norm_completedHurwitzZetaEven_zero_growth_of_Lambda_zero_growth line 455
  27. theorem OAI.SiegelZeros.WeightedTorusJets.norm_completedHurwitzZetaOdd_growth_of_Lambda_zero_growth line 466
  28. theorem OAI.SiegelZeros.WeightedTorusJets.exists_completedHurwitzZetaEven_zero_growth line 481
  29. theorem OAI.SiegelZeros.WeightedTorusJets.exists_completedHurwitzZetaOdd_growth line 489