OAI/NumberTheory/DirichletL/Moments/HeckeExpansion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentHeckeExpansion.rowWeight line 13
  2. theorem OAI.SevenEighths.CenteredMomentHeckeExpansion.rowTwistedSum_eq_weight line 27
  3. theorem OAI.SevenEighths.CenteredMomentHeckeExpansion.rowSlot_eq_weight line 31
  4. theorem OAI.SevenEighths.CenteredMomentHeckeExpansion.actual_hecke_rectangle_sum line 40
  5. theorem OAI.SevenEighths.CenteredMomentHeckeExpansion.live_slot_product line 76
  6. theorem OAI.SevenEighths.CenteredMomentHeckeExpansion.actual_slot_rectangle_sum line 90
  7. theorem OAI.SevenEighths.CenteredMomentHeckeExpansion.common_extracted_slot_rectangle line 117