OAI/NumberTheory/Ostmann/Dirichlet/GrowthBase.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Dirichlet.sum_character_period_eq_zero line 21
  2. theorem OAI.Ostmann.Dirichlet.norm_sum_character_range_lt line 48
  3. theorem OAI.Ostmann.Dirichlet.norm_sum_character_Icc_lt line 77
  4. theorem OAI.Ostmann.Dirichlet.isBigO_sum_character_Icc_one line 98
  5. theorem OAI.Ostmann.Dirichlet.mellin_partial_sum_neg line 118
  6. theorem OAI.Ostmann.Dirichlet.differentiableAt_partial_sum_integral line 147
  7. theorem OAI.Ostmann.Dirichlet.LFunction_eq_partial_sum_integral line 195
  8. theorem OAI.Ostmann.Dirichlet.LFunction_eq_partial_sum_integral_of_re_pos line 216