OAI/NumberTheory/DirichletL/Descent/Completion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseMoment.markedCompletedT line 15
  2. theorem OAI.SevenEighths.InverseMoment.markedCompletedT_one line 19
  3. theorem OAI.SevenEighths.InverseMoment.markedCompletedT_congr_nonzero line 23
  4. theorem OAI.SevenEighths.InverseMoment.markedCompletedT_summable line 36
  5. theorem OAI.SevenEighths.InverseMoment.markedCompletedT_eq_tsum line 45
  6. theorem OAI.SevenEighths.InverseMoment.markedCompletedT_const_mul line 51
  7. theorem OAI.SevenEighths.InverseMoment.markedCompletedT_finset_sum line 56
  8. theorem OAI.SevenEighths.InverseMoment.markedCompletedT_prime_priority line 64
  9. def OAI.SevenEighths.InverseMoment.markedExpandedTerm line 91
  10. theorem OAI.SevenEighths.InverseMoment.markedExpandedTerm_finite_support line 95
  11. theorem OAI.SevenEighths.InverseMoment.markedExpandedTerm_scale line 104
  12. theorem OAI.SevenEighths.InverseMoment.weighted_markedCompletedT_reopen line 114
  13. theorem OAI.SevenEighths.InverseMoment.marked_cube_inner_inverse line 121
  14. theorem OAI.SevenEighths.InverseMoment.marked_cube_inverse_vstar line 146
  15. theorem OAI.SevenEighths.InverseMoment.marked_cube_inverse line 180