OAI/Computability/FourierCircuit/DiagonalBlocks.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.diagonalBlocks line 10
  2. theorem OAI.ExactFourier.MatrixPrice.diagonal_blocks line 16
  3. def OAI.ExactFourier.RootEvaluation.fourier line 50
  4. theorem OAI.ExactFourier.RootEvaluation.fourier_mulVec line 53
  5. theorem OAI.ExactFourier.RootEvaluation.fourier_unit line 56
  6. theorem OAI.ExactFourier.RootEvaluation.fourier_price line 66
  7. def OAI.ExactFourier.RootEvaluation.matrix line 83
  8. theorem OAI.ExactFourier.RootEvaluation.matrix_eq line 86
  9. theorem OAI.ExactFourier.RootEvaluation.matrix_unit line 91
  10. theorem OAI.ExactFourier.RootEvaluation.matrix_price line 97
  11. theorem OAI.ExactFourier.RootEvaluation.coefficient_sum line 114
  12. theorem OAI.ExactFourier.RootEvaluation.eval_remainder line 124
  13. theorem OAI.ExactFourier.RootEvaluation.intertwine line 130
  14. theorem OAI.ExactFourier.RootEvaluation.root_modulus line 153
  15. theorem OAI.ExactFourier.RootEvaluation.modulus_upper line 169
  16. theorem OAI.ExactFourier.RootEvaluation.exists_dilation line 217
  17. theorem OAI.ExactFourier.exists_dyadic_between line 241
  18. theorem OAI.ExactFourier.fixed_price_of_dyadic_boundary line 247
  19. theorem OAI.ExactFourier.MatrixPrice.specialize_polynomial_zero line 306