OAI/NumberTheory/DirichletL/Moments/Basic.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.CenteredMoment.MaskedCharacter line 19
  2. def OAI.SevenEighths.CenteredMoment.ofResidueMask line 25
  3. theorem OAI.SevenEighths.CenteredMoment.ofResidueMask_keep_one line 34
  4. def OAI.SevenEighths.CenteredMoment.MaskedCharacter.value line 40
  5. theorem OAI.SevenEighths.CenteredMoment.MaskedCharacter.value_mul line 43
  6. def OAI.SevenEighths.CenteredMoment.normTwist line 49
  7. theorem OAI.SevenEighths.CenteredMoment.normTwist_mul line 52
  8. def OAI.SevenEighths.CenteredMoment.coefficient line 57
  9. theorem OAI.SevenEighths.CenteredMoment.coefficient_mul line 60
  10. def OAI.SevenEighths.CenteredMoment.plainSum line 66
  11. def OAI.SevenEighths.CenteredMoment.rectangle line 70
  12. theorem OAI.SevenEighths.CenteredMoment.rectangle_sum_eq line 75
  13. theorem OAI.SevenEighths.CenteredMoment.slot_rectangle_sum_eq line 89
  14. def OAI.SevenEighths.CenteredMoment.volumeTerm line 99
  15. theorem OAI.SevenEighths.CenteredMoment.volume_products_eq line 102
  16. theorem OAI.SevenEighths.CenteredMoment.centered_error_identity line 119
  17. theorem OAI.SevenEighths.CenteredMoment.norm_centered_le line 126
  18. theorem OAI.SevenEighths.CenteredMoment.norm_centered_le_of_approx line 143
  19. theorem OAI.SevenEighths.CenteredMoment.scale_le_product_div line 160
  20. theorem OAI.SevenEighths.CenteredMoment.sum_scales_le line 167
  21. theorem OAI.SevenEighths.CenteredMoment.centered_saving_of_approx line 180
  22. theorem OAI.SevenEighths.CenteredMoment.extracted_volume_phase line 201
  23. theorem OAI.SevenEighths.CenteredMoment.extracted_volume_sum line 211
  24. theorem OAI.SevenEighths.CenteredMoment.centered_volume_fallback line 227
  25. theorem OAI.SevenEighths.CenteredMoment.normalized_centered_saving line 243