OAI/NumberTheory/DirichletL/Moments/DetectorPlainSlotProfile.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.conjugate_source_support line 17
  2. lemma OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.conjugate_source_smooth line 22
  3. def OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.slotSchwartz line 26
  4. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.slotSchwartz_apply line 31
  5. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.slotSchwartz_support line 43
  6. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.slotSchwartz_smooth line 50
  7. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.slotSchwartz_norm line 53
  8. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.physical_coefficient line 69
  9. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.physical_coefficient_norm line 76
  10. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.slotSchwartz_uniform line 83
  11. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.slotSchwartz_height_uniform line 93
  12. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSlotProfile.physical_positive_row line 104