OAI/NumberTheory/DirichletL/Moments/HeckeColumnWindow.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentHeckeColumnWindow.heightCoeff line 15
  2. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.heightCoeff_add line 18
  3. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.heightCoeff_phase line 24
  4. def OAI.SevenEighths.CenteredMomentHeckeColumnWindow.rootProfile line 34
  5. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.rootProfile_apply line 39
  6. def OAI.SevenEighths.CenteredMomentHeckeColumnWindow.columnDensity line 46
  7. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.columnDensity_moments line 49
  8. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.rootWindow_integral line 54
  9. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.phase_combine line 65
  10. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.height_column_integral line 73
  11. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.height_column_integrable line 91
  12. theorem OAI.SevenEighths.CenteredMomentHeckeColumnWindow.gauss_column_integral line 116