OAI/NumberTheory/DirichletL/Detector/CanonicalSlots.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbePhysical.canonicalSlotSupport line 12
  2. lemma OAI.SevenEighths.ProbePhysical.primaryPrime_injective line 15
  3. lemma OAI.SevenEighths.ProbePhysical.canonicalSlotSupport_nonzero line 21
  4. def OAI.SevenEighths.ProbePhysical.canonicalSlotEquiv line 26
  5. lemma OAI.SevenEighths.ProbePhysical.canonicalSlotEquiv_val line 38
  6. lemma OAI.SevenEighths.ProbePhysical.canonicalSlotEquiv_span line 41
  7. lemma OAI.SevenEighths.ProbePhysical.canonicalSlotEquiv_norm line 45
  8. def OAI.SevenEighths.ProbePhysical.canonicalTupleEquiv line 49
  9. lemma OAI.SevenEighths.ProbePhysical.canonicalTupleEquiv_val line 54
  10. theorem OAI.SevenEighths.ProbePhysical.sum_canonical_element_tuples line 58
  11. lemma OAI.SevenEighths.ProbePhysical.canonicalSlotSupport_disjoint line 65
  12. lemma OAI.SevenEighths.ProbePhysical.idealTuple_injective_of_disjoint line 75
  13. lemma OAI.SevenEighths.ProbePhysical.canonicalElementTuple_injective_of_disjoint line 84
  14. theorem OAI.SevenEighths.ProbePhysical.sum_canonical_weighted_tuples line 92
  15. def OAI.SevenEighths.ProbePhysical.idealSlotOfPrimary line 104
  16. lemma OAI.SevenEighths.ProbePhysical.idealSlotOfPrimary_supported line 107
  17. lemma OAI.SevenEighths.ProbePhysical.primarySlotNormalization line 114
  18. lemma OAI.SevenEighths.ProbePhysical.canonicalSlotSupport_disjoint_iff line 139
  19. lemma OAI.SevenEighths.ProbePhysical.originalPrimarySlots_disjoint line 150
  20. theorem OAI.SevenEighths.ProbePhysical.sum_original_primary_weighted_tuples line 160