OAI/NumberTheory/DirichletL/Moments/RowNorm.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentRowNorm.pairResidue line 15
  2. theorem OAI.SevenEighths.CenteredMomentRowNorm.pairResidue_mk line 21
  3. def OAI.SevenEighths.CenteredMomentRowNorm.pairFourier line 27
  4. theorem OAI.SevenEighths.CenteredMomentRowNorm.row_pair_summable line 33
  5. theorem OAI.SevenEighths.CenteredMomentRowNorm.row_pair_poisson line 45
  6. def OAI.SevenEighths.CenteredMomentRowNorm.rowPolynomial line 61
  7. def OAI.SevenEighths.CenteredMomentRowNorm.rowEnergy line 64
  8. theorem OAI.SevenEighths.CenteredMomentRowNorm.rowPolynomial_norm_sq line 69
  9. theorem OAI.SevenEighths.CenteredMomentRowNorm.rowEnergy_expand line 84
  10. theorem OAI.SevenEighths.CenteredMomentRowNorm.rowEnergy_poisson line 101