OAI/NumberTheory/DirichletL/Moments/FirstPhysicalActiveDictionary.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.columns_active line 22
  2. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.element_value line 30
  3. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.column_sum_active line 34
  4. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.column_pair_sum_active line 44
  5. lemma OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.primary_supported line 54
  6. def OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.physicalTerm line 59
  7. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.physicalTerm_zero_left line 86
  8. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.physicalTerm_zero_right line 94
  9. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.block_eq_ideal_sums line 102
  10. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.block_active line 131
  11. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.block_active_ne_zero_iff line 146
  12. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.original_dyadic_block_active line 160
  13. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.original_sector_active line 173
  14. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.original_sectorMass_active line 188
  15. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.original_retained_full_sectorMass line 203
  16. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.active_sectorMass_sum line 218
  17. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.physicalMass_full_source line 232
  18. theorem OAI.SevenEighths.CenteredMomentFirstPhysicalActiveDictionary.normalized_physicalMass_full_source line 246