OAI/NumberTheory/DirichletL/Moments/ReflectionMass.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentReflectionMass.weight line 12
  2. lemma OAI.SevenEighths.CenteredMomentReflectionMass.weight_nonneg line 13
  3. lemma OAI.SevenEighths.CenteredMomentReflectionMass.weight_mul line 14
  4. lemma OAI.SevenEighths.CenteredMomentReflectionMass.weight_one line 17
  5. lemma OAI.SevenEighths.CenteredMomentReflectionMass.weight_pow line 18
  6. lemma OAI.SevenEighths.CenteredMomentReflectionMass.weight_prod line 22
  7. lemma OAI.SevenEighths.CenteredMomentReflectionMass.prime_weight_lt_one line 27
  8. def OAI.SevenEighths.CenteredMomentReflectionMass.exponents line 36
  9. lemma OAI.SevenEighths.CenteredMomentReflectionMass.reconstruct_exponents line 38
  10. lemma OAI.SevenEighths.CenteredMomentReflectionMass.exponents_injective line 44
  11. lemma OAI.SevenEighths.CenteredMomentReflectionMass.weight_exponents line 49
  12. lemma OAI.SevenEighths.CenteredMomentReflectionMass.hasSum_geometric_pi line 57
  13. lemma OAI.SevenEighths.CenteredMomentReflectionMass.smooth_summable line 84
  14. lemma OAI.SevenEighths.CenteredMomentReflectionMass.smooth_mass_le_euler line 90
  15. lemma OAI.SevenEighths.CenteredMomentReflectionMass.deletion_mass line 100
  16. def OAI.SevenEighths.CenteredMomentReflectionMass.localMass line 105
  17. lemma OAI.SevenEighths.CenteredMomentReflectionMass.localMass_nonneg line 106
  18. lemma OAI.SevenEighths.CenteredMomentReflectionMass.prime_weight_le line 108
  19. lemma OAI.SevenEighths.CenteredMomentReflectionMass.localMass_le_seven line 116
  20. lemma OAI.SevenEighths.CenteredMomentReflectionMass.localMass_le_three line 119
  21. theorem OAI.SevenEighths.CenteredMomentReflectionMass.euler_mass_subpower line 130
  22. def OAI.SevenEighths.CenteredMomentReflectionMass.coefficient line 170
  23. lemma OAI.SevenEighths.CenteredMomentReflectionMass.coefficient_norm_le line 175
  24. lemma OAI.SevenEighths.CenteredMomentReflectionMass.coefficient_summable_norm line 188
  25. lemma OAI.SevenEighths.CenteredMomentReflectionMass.coefficient_summable line 195
  26. lemma OAI.SevenEighths.CenteredMomentReflectionMass.coefficient_mass_le_euler line 199
  27. lemma OAI.SevenEighths.CenteredMomentReflectionMass.coefficient_mass_summable line 218
  28. theorem OAI.SevenEighths.CenteredMomentReflectionMass.reflection_mass_subpower line 223
  29. def OAI.SevenEighths.CenteredMomentReflectionMass.unitSmooth line 233
  30. lemma OAI.SevenEighths.CenteredMomentReflectionMass.coefficient_empty_unit line 238
  31. lemma OAI.SevenEighths.CenteredMomentReflectionMass.reflectedTerm_eq_coefficient line 248