OAI/Computability/FourierCircuit/MatrixRelabel.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.reindex_mulVec line 8
  2. def OAI.ExactFourier.RadixTwo.dft line 22
  3. def OAI.ExactFourier.RadixTwo.butterfly line 24
  4. theorem OAI.ExactFourier.RadixTwo.butterfly_layer line 27
  5. def OAI.ExactFourier.RadixTwo.paritySumEquiv line 45
  6. theorem OAI.ExactFourier.RadixTwo.paritySumEquiv_inl line 48
  7. theorem OAI.ExactFourier.RadixTwo.paritySumEquiv_inr line 50
  8. theorem OAI.ExactFourier.RadixTwo.dft_step line 53
  9. theorem OAI.ExactFourier.RadixTwo.dft_layers line 75
  10. def OAI.ExactFourier.NewtonFourier.newton line 108
  11. def OAI.ExactFourier.NewtonFourier.H line 109
  12. def OAI.ExactFourier.NewtonFourier.scale line 110
  13. def OAI.ExactFourier.NewtonFourier.N line 111
  14. def OAI.ExactFourier.NewtonFourier.P line 112
  15. theorem OAI.ExactFourier.NewtonFourier.newton_zero line 114
  16. theorem OAI.ExactFourier.NewtonFourier.newton_succ line 115
  17. theorem OAI.ExactFourier.NewtonFourier.H_zero line 117
  18. theorem OAI.ExactFourier.NewtonFourier.H_succ line 118
  19. theorem OAI.ExactFourier.NewtonFourier.scale_zero line 119
  20. theorem OAI.ExactFourier.NewtonFourier.scale_succ line 120
  21. theorem OAI.ExactFourier.NewtonFourier.newton_monic line 122
  22. theorem OAI.ExactFourier.NewtonFourier.newton_natDegree line 123
  23. theorem OAI.ExactFourier.NewtonFourier.newton_eval_zero line 128
  24. theorem OAI.ExactFourier.NewtonFourier.eval_factor line 132
  25. theorem OAI.ExactFourier.NewtonFourier.H_ne_zero line 147
  26. theorem OAI.ExactFourier.NewtonFourier.scale_ne_zero line 153
  27. theorem OAI.ExactFourier.NewtonFourier.N_lower line 158
  28. theorem OAI.ExactFourier.NewtonFourier.P_upper line 162
  29. theorem OAI.ExactFourier.NewtonFourier.dft_mul_P line 166
  30. theorem OAI.ExactFourier.Layered.inverse line 183
  31. theorem OAI.ExactFourier.Layered.conjugate line 199
  32. theorem OAI.ExactFourier.Layered.rect_diagonal line 213
  33. theorem OAI.ExactFourier.Layered.rect_add line 229
  34. theorem OAI.ExactFourier.Layered.rect_neg line 235
  35. theorem OAI.ExactFourier.Layered.rect_mul_left line 240
  36. theorem OAI.ExactFourier.Layered.rect_mul_right line 251
  37. def OAI.ExactFourier.Layered.swapLast line 273
  38. theorem OAI.ExactFourier.Layered.rect_first line 276
  39. theorem OAI.ExactFourier.Layered.rect_last line 285
  40. theorem OAI.ExactFourier.Layered.commutator_identity line 294
  41. theorem OAI.ExactFourier.Layered.rect_product_stable line 307
  42. theorem OAI.ExactFourier.Layered.rect_transpose line 332
  43. theorem OAI.ExactFourier.Layered.embedded_injection line 342
  44. theorem OAI.ExactFourier.Layered.rect_injection line 384
  45. theorem OAI.ExactFourier.Layered.rect_projection line 390
  46. theorem OAI.ExactFourier.Layered.rect_submatrix_stable line 393