OAI/Computability/FourierCircuit/PolynomialClearing.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Exact finite Taylor change of coefficient basis.

  1. theorem OAI.ExactFourier.Boundary.time_power_clearing line 12
  2. theorem OAI.ExactFourier.Boundary.time_power_clearing_price line 24
  3. def OAI.ExactFourier.Taylor.matrix line 55
  4. theorem OAI.ExactFourier.Taylor.coefficient_sum line 58
  5. theorem OAI.ExactFourier.Taylor.matrix_mul line 67
  6. theorem OAI.ExactFourier.Taylor.matrix_zero line 76
  7. theorem OAI.ExactFourier.Taylor.matrix_unit line 81
  8. theorem OAI.ExactFourier.Taylor.matrix_inv line 86
  9. theorem OAI.ExactFourier.Taylor.taylor_modulus line 90
  10. theorem OAI.ExactFourier.Taylor.remainder_coeff line 93
  11. def OAI.ExactFourier.Taylor.translate line 101
  12. theorem OAI.ExactFourier.Taylor.intertwine line 104
  13. def OAI.ExactFourier.Taylor.kernel line 147
  14. theorem OAI.ExactFourier.Taylor.kernel_constant line 150
  15. theorem OAI.ExactFourier.Taylor.diagonal_factorization line 153
  16. theorem OAI.ExactFourier.Taylor.price line 170
  17. theorem OAI.ExactFourier.Taylor.conjugacy line 180
  18. theorem OAI.ExactFourier.Taylor.modulus_unit line 189
  19. theorem OAI.ExactFourier.Taylor.modulus_lower line 209
  20. def OAI.ExactFourier.CellPoly.feedback line 239
  21. theorem OAI.ExactFourier.CellPoly.eval_Z line 243
  22. theorem OAI.ExactFourier.CellPoly.eval_a line 253
  23. theorem OAI.ExactFourier.CellPoly.eval_R line 257
  24. theorem OAI.ExactFourier.CellPoly.adjugate_eq_det_smul_inv line 262
  25. theorem OAI.ExactFourier.CellPoly.eval_F line 269
  26. def OAI.ExactFourier.boundaryError line 292
  27. theorem OAI.ExactFourier.boundaryError_tendsto line 296
  28. theorem OAI.ExactFourier.fixed_price_of_boundary line 320
  29. theorem OAI.ExactFourier.MatrixPrice.feedback line 345