OAI/Computability/FourierCircuit/PairFamilies.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.PairFamily.sumEquiv line 12
  2. theorem OAI.ExactFourier.PairFamily.sum_blocks line 18
  3. def OAI.ExactFourier.PairFamily.subEmbedding line 31
  4. theorem OAI.ExactFourier.PairFamily.sub_blocks line 35
  5. theorem OAI.ExactFourier.PairFamily.split_blocks line 64
  6. structure OAI.ExactFourier.PairFamily line 76

    Source documentation

    A simultaneous pair family retains its actual disjoint ordered coordinate tuples.

    structure PairFamily (α : Type) [Fintype α] [DecidableEq α] where
…
  7. def OAI.ExactFourier.PairFamily.matrix line 86
  8. def OAI.ExactFourier.PairFamily.empty line 87
  9. theorem OAI.ExactFourier.PairFamily.empty_matrix line 94
  10. def OAI.ExactFourier.PairFamily.pair line 99
  11. theorem OAI.ExactFourier.PairFamily.pair_matrix line 106
  12. def OAI.ExactFourier.PairFamily.reindex line 113
  13. theorem OAI.ExactFourier.PairFamily.reindex_matrix line 115
  14. def OAI.ExactFourier.PairFamily.sum line 120
  15. theorem OAI.ExactFourier.PairFamily.sum_matrix line 127
  16. theorem OAI.ExactFourier.PairFamily.card_le line 132
  17. theorem OAI.ExactFourier.Round.pair_rep line 139
  18. theorem OAI.ExactFourier.AGenerated.blocks_fin line 162
  19. theorem OAI.ExactFourier.AGenerated.blocks line 183
  20. theorem OAI.ExactFourier.AGenerated.blockDiagonal line 203
  21. theorem OAI.ExactFourier.PairFamily.one_batch line 227
  22. theorem OAI.ExactFourier.PairFamily.batches line 239
  23. theorem OAI.ExactFourier.PairFamily.generated line 274
  24. theorem OAI.ExactFourier.Round.generated line 291
  25. theorem OAI.ExactFourier.Layered.generated line 302
  26. theorem OAI.ExactFourier.AGenerated.zero line 328
  27. theorem OAI.ExactFourier.AGenerated.succ line 333
  28. theorem OAI.ExactFourier.ParallelTensorCost.frames_cost line 350
  29. theorem OAI.ExactFourier.ParallelTensorCost.generated_cost line 363
  30. theorem OAI.ExactFourier.ParallelTensorCost.layered_cost line 381