OAI/NumberTheory/DirichletL/ThetaRegularity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.ThetaRegularity.O line 15
  2. theorem OAI.SevenEighths.ThetaRegularity.norm_gaussian line 19
  3. theorem OAI.SevenEighths.ThetaRegularity.lattice_gap line 23
  4. theorem OAI.SevenEighths.ThetaRegularity.gaussian_le_inverse_square line 29
  5. def OAI.SevenEighths.ThetaRegularity.decayRate line 49
  6. theorem OAI.SevenEighths.ThetaRegularity.decayRate_pos line 51
  7. theorem OAI.SevenEighths.ThetaRegularity.parameter_eq line 55
  8. theorem OAI.SevenEighths.ThetaRegularity.norm_gaussian_parameter line 60
  9. theorem OAI.SevenEighths.ThetaRegularity.coefficient_norm_le_one line 67
  10. theorem OAI.SevenEighths.ThetaRegularity.term_norm_le line 78
  11. theorem OAI.SevenEighths.ThetaRegularity.continuousOn_theta_above line 85
  12. theorem OAI.SevenEighths.ThetaRegularity.continuousAt_theta line 101
  13. theorem OAI.SevenEighths.ThetaRegularity.continuousOn_theta line 106
  14. theorem OAI.SevenEighths.ThetaRegularity.theta_locallyIntegrableOn line 110
  15. def OAI.SevenEighths.ThetaRegularity.tailConstant line 114
  16. theorem OAI.SevenEighths.ThetaRegularity.tailConstant_nonneg line 117
  17. theorem OAI.SevenEighths.ThetaRegularity.tailConstant_le_cauchy line 119
  18. theorem OAI.SevenEighths.ThetaRegularity.tailConstant_le_linear line 128
  19. theorem OAI.SevenEighths.ThetaRegularity.tail_eq_tsum line 141
  20. theorem OAI.SevenEighths.ThetaRegularity.tail_term_bound line 148
  21. theorem OAI.SevenEighths.ThetaRegularity.theta_tail_bound line 169
  22. theorem OAI.SevenEighths.ThetaRegularity.theta_tail_bound_conductor line 182
  23. theorem OAI.SevenEighths.ThetaRegularity.theta_tail_isBigO_exp line 190
  24. theorem OAI.SevenEighths.ThetaRegularity.theta_tail_isBigO_rpow line 199