OAI/NumberTheory/DirichletL/Hecke/EulerLog.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeEulerLog.eulerLog line 16
  2. def OAI.SevenEighths.HeckeEulerLog.majorant line 19
  3. theorem OAI.SevenEighths.HeckeEulerLog.majorant_summable line 22
  4. theorem OAI.SevenEighths.HeckeEulerLog.weighted_norm_le line 31
  5. theorem OAI.SevenEighths.HeckeEulerLog.weighted_norm_le_half line 44
  6. theorem OAI.SevenEighths.HeckeEulerLog.log_factor_norm_le line 52
  7. theorem OAI.SevenEighths.HeckeEulerLog.weighted_differentiable line 61
  8. theorem OAI.SevenEighths.HeckeEulerLog.log_factor_differentiableOn line 69
  9. theorem OAI.SevenEighths.HeckeEulerLog.eulerLog_differentiableOn_halfplane line 81
  10. theorem OAI.SevenEighths.HeckeEulerLog.eulerLog_differentiableOn line 90
  11. theorem OAI.SevenEighths.HeckeEulerLog.exp_eulerLog_eq_series line 99
  12. def OAI.SevenEighths.HeckeEulerLog.eulerLogBound line 103
  13. theorem OAI.SevenEighths.HeckeEulerLog.eulerLogBound_ge_one line 105
  14. theorem OAI.SevenEighths.HeckeEulerLog.eulerLog_norm_le line 111
  15. theorem OAI.SevenEighths.HeckeEulerLog.inner_disk_re line 124
  16. theorem OAI.SevenEighths.HeckeEulerLog.eulerLog_inner_disk line 132
  17. theorem OAI.SevenEighths.HeckeEulerLog.continued_inner_disk line 149
  18. def OAI.SevenEighths.HeckeEulerLog.principalLog line 161
  19. theorem OAI.SevenEighths.HeckeEulerLog.norm_two_div_add_one_lt_one line 163
  20. theorem OAI.SevenEighths.HeckeEulerLog.norm_two_div_add_one_le line 172
  21. theorem OAI.SevenEighths.HeckeEulerLog.principalLog_differentiableOn line 181
  22. theorem OAI.SevenEighths.HeckeEulerLog.exp_principalLog line 198
  23. theorem OAI.SevenEighths.HeckeEulerLog.principalLog_norm_le line 210
  24. def OAI.SevenEighths.HeckeEulerLog.principalEulerLog line 228
  25. theorem OAI.SevenEighths.HeckeEulerLog.principalEulerLog_differentiableOn line 230
  26. theorem OAI.SevenEighths.HeckeEulerLog.exp_principalEulerLog line 234
  27. theorem OAI.SevenEighths.HeckeEulerLog.principalEulerLog_norm_le line 239
  28. theorem OAI.SevenEighths.HeckeEulerLog.principal_continued_inner_disk line 243
  29. theorem OAI.SevenEighths.HeckeEulerLog.residue_continued_inner_disk line 263
  30. theorem OAI.SevenEighths.HeckeEulerLog.continued_logarithmic_control line 274
  31. theorem OAI.SevenEighths.HeckeEulerLog.principal_continued_logarithmic_control line 296