OAI/NumberTheory/Ostmann/Characters/HistoryArchimedeanVariationProduct.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Ostmann.Characters.HistoryProfile line 9
  2. def OAI.Ostmann.Characters.HistoryProfile.eval line 13
  3. def OAI.Ostmann.Characters.HistoryProfile.bound line 17
  4. theorem OAI.Ostmann.Characters.HistoryProfile.bound_pos line 21
  5. theorem OAI.Ostmann.Characters.HistoryProfile.norm_eval_le line 27
  6. theorem OAI.Ostmann.Characters.HistoryProfile.eval_lipschitz line 33
  7. theorem OAI.Ostmann.Characters.norm_finset_product_sub_le line 40
  8. def OAI.Ostmann.Characters.historyArchimedeanProduct line 69
  9. theorem OAI.Ostmann.Characters.historyArchimedeanProduct_norm_le line 73
  10. theorem OAI.Ostmann.Characters.historyArchimedeanProduct_difference_le line 86