OAI/NumberTheory/DirichletL/Moments/ReflectionWeightedEnergy.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.Index line 13
  2. def OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.baseIndex line 15
  3. def OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.signedWeight line 18
  4. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.signedWeight_norm line 22
  5. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.annularMass_le_two line 28
  6. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.coefficient_joint_summable line 35
  7. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.coefficient_joint_mass line 43
  8. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.signedWeight_summable_norm line 50
  9. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.signedWeight_mass line 57
  10. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.signed_series_reindex line 66
  11. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.signedWeight_base line 74
  12. theorem OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.signed_mass_subpower line 78
  13. def OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.annularConstant line 91
  14. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.annularConstant_pos line 93
  15. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.annularMass_total_le line 98
  16. theorem OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.uniform_signed_mass line 105
  17. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.sum_iSup_le_of_selection line 117
  18. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.selection_point_bound line 141
  19. theorem OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.weighted_selection_energy line 151
  20. theorem OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.finite_weighted_selection_energy line 186
  21. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.masked_signedWeight_summable_norm line 212
  22. lemma OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.masked_signedWeight_mass_le line 221
  23. theorem OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.actual_masked_reflection_energy line 231
  24. theorem OAI.SevenEighths.CenteredMomentReflectionWeightedEnergy.actual_reflection_energy line 266