OAI/Computability/FourierCircuit/SumFramed.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactFourier.Packing.SumDomain line 15
  2. instance OAI.ExactFourier.Packing.SumDomain_fintype line 18
  3. instance OAI.ExactFourier.Packing.SumDomain_decEq line 20
  4. def OAI.ExactFourier.Packing.sumFramed line 23
  5. def OAI.ExactFourier.Packing.sumTime line 28
  6. theorem OAI.ExactFourier.Packing.sumTime_strict line 35
  7. theorem OAI.ExactFourier.Packing.sum_slot_card line 45
  8. theorem OAI.ExactFourier.Packing.matrix_sumFramed line 71
  9. def OAI.ExactFourier.Packing.emptyFramed line 99
  10. theorem OAI.ExactFourier.Packing.emptyFramed_matrix line 101
  11. def OAI.ExactFourier.Packing.emptyTime line 105
  12. theorem OAI.ExactFourier.Packing.emptyTime_strict line 107
  13. theorem OAI.ExactFourier.Packing.empty_slot_card line 111
  14. theorem OAI.ExactFourier.Packing.list_count_get line 126
  15. theorem OAI.ExactFourier.Packing.list_card_get line 137
  16. theorem OAI.ExactFourier.Packing.list_count_map_get line 142
  17. theorem OAI.ExactFourier.Packing.slot_card_sum line 166
  18. theorem OAI.ExactFourier.Packing.slot_card_total line 175
  19. theorem OAI.ExactFourier.Packing.complete_and_pack line 209
  20. def OAI.ExactFourier.Packing.cyclicTime line 313
  21. theorem OAI.ExactFourier.Packing.cyclicTime_strict line 319
  22. theorem OAI.ExactFourier.Packing.cyclic_slot_card line 326
  23. theorem OAI.ExactFourier.Packing.cyclic_slot_bound line 350