OAI/NumberTheory/DirichletL/Moments/SourceRow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentSourceRow.rowWeight_split line 14
  2. theorem OAI.SevenEighths.CenteredMomentSourceRow.rowWeight_zero_of_not_supported line 21
  3. def OAI.SevenEighths.CenteredMomentSourceRow.supportedColumns line 39
  4. theorem OAI.SevenEighths.CenteredMomentSourceRow.primary_span_supported line 41
  5. def OAI.SevenEighths.CenteredMomentSourceRow.sourceGenerator line 49
  6. theorem OAI.SevenEighths.CenteredMomentSourceRow.sourceGenerator_supported line 51
  7. theorem OAI.SevenEighths.CenteredMomentSourceRow.finite_hecke_sum_eq_rowPolynomial line 57
  8. def OAI.SevenEighths.CenteredMomentSourceRow.finiteHeckeEnergy line 77
  9. theorem OAI.SevenEighths.CenteredMomentSourceRow.finiteHeckeEnergy_eq line 82
  10. theorem OAI.SevenEighths.CenteredMomentSourceRow.finiteHeckeEnergy_poisson line 91