OAI/Computability/FourierCircuit/RectStableAlgebra.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.Layered.stable_rect_add line 11
  2. theorem OAI.ExactFourier.Layered.stable_rect_transpose line 18
  3. def OAI.ExactFourier.Layered.splitRowsLeft line 32
  4. def OAI.ExactFourier.Layered.splitRowsRight line 46
  5. theorem OAI.ExactFourier.Layered.split_rows_left_matrix line 50
  6. theorem OAI.ExactFourier.Layered.split_rows_right_matrix line 59
  7. theorem OAI.ExactFourier.Layered.stable_rect_split_rows line 68
  8. theorem OAI.ExactFourier.Layered.stable_reindex line 94
  9. theorem OAI.ExactFourier.Layered.stable_extra line 108
  10. theorem OAI.ExactFourier.Layered.stable_scratch_mono line 121
  11. theorem OAI.ExactFourier.Layered.stable_zero line 129
  12. theorem OAI.ExactFourier.Layered.stable_empty_rows line 139
  13. theorem OAI.ExactFourier.Layered.stable_empty_cols line 148
  14. theorem OAI.ExactFourier.Layered.stable_rows_nat line 152
  15. def OAI.ExactFourier.SumLayered line 186
  16. theorem OAI.ExactFourier.SumLayered.single line 190
  17. theorem OAI.ExactFourier.SumLayered.weaken line 192
  18. theorem OAI.ExactFourier.SumLayered.add line 196
  19. theorem OAI.ExactFourier.SumLayered.transpose line 205
  20. theorem OAI.ExactFourier.SumLayered.mul line 215
  21. theorem OAI.ExactFourier.SumLayered.diagonal line 239
  22. theorem OAI.ExactFourier.SumLayered.submatrix_stable line 254
  23. def OAI.ExactFourier.RadixTwo.convolutionMatrix line 287
  24. theorem OAI.ExactFourier.RadixTwo.convolution_sumLayered line 291
  25. theorem OAI.ExactFourier.RadixTwo.convolution_mulVec line 298
  26. theorem OAI.ExactFourier.RadixTwo.ofFn_single line 314
  27. theorem OAI.ExactFourier.RadixTwo.convolution_entry line 324
  28. def OAI.ExactFourier.initialEmbedding line 345
  29. theorem OAI.ExactFourier.initialEmbedding_val line 348
  30. theorem OAI.ExactFourier.sum_initial line 351
  31. theorem OAI.ExactFourier.compress_product line 369