OAI/Computability/FourierCircuit/CascadeWord.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Polynomial clearing for the cascade (05-corners:327–369). No inverse of D and no genericity of evaluation points is used.

  1. abbrev OAI.ExactFourier.Cascade.States line 11
  2. instance OAI.ExactFourier.Cascade.statesFintype line 14
  3. instance OAI.ExactFourier.Cascade.statesDecidableEq line 19
  4. def OAI.ExactFourier.Cascade.response line 27
  5. def OAI.ExactFourier.Cascade.run line 32
  6. theorem OAI.ExactFourier.Cascade.unit line 38
  7. theorem OAI.ExactFourier.Cascade.price line 46
  8. theorem OAI.ExactFourier.Cascade.data_block line 68
  9. theorem OAI.ExactFourier.Cascade.columns_fromCols line 84
  10. theorem OAI.ExactFourier.Cascade.state_block line 90
  11. abbrev OAI.ExactFourier.CellPoly.ps line 119
  12. theorem OAI.ExactFourier.CellPoly.map_smul line 121
  13. def OAI.ExactFourier.CellPoly.Z line 126
  14. def OAI.ExactFourier.CellPoly.a line 128
  15. def OAI.ExactFourier.CellPoly.R line 129
  16. def OAI.ExactFourier.CellPoly.F line 130
  17. def OAI.ExactFourier.CellPoly.b line 134
  18. def OAI.ExactFourier.CellPoly.J line 136
  19. def OAI.ExactFourier.CellPoly.L line 138
  20. def OAI.ExactFourier.CellPoly.T line 140
  21. theorem OAI.ExactFourier.CellPoly.map_const line 144
  22. theorem OAI.ExactFourier.CellPoly.map_Z line 146
  23. theorem OAI.ExactFourier.CellPoly.eval_Z_zero line 152
  24. theorem OAI.ExactFourier.CellPoly.eval_a_zero line 156
  25. theorem OAI.ExactFourier.CellPoly.eval_F_zero line 159
  26. theorem OAI.ExactFourier.CellPoly.eval_b_zero line 166
  27. theorem OAI.ExactFourier.CellPoly.cleared_resolvent line 171
  28. theorem OAI.ExactFourier.CellPoly.cleared_state line 183
  29. theorem OAI.ExactFourier.CellPoly.cleared_transfer line 188
  30. theorem OAI.ExactFourier.CellPoly.right_clearing line 196
  31. theorem OAI.ExactFourier.CellPoly.state_clearing line 204
  32. theorem OAI.ExactFourier.Cascade.power_smul line 229
  33. def OAI.ExactFourier.Cascade.cleared line 238
  34. theorem OAI.ExactFourier.Cascade.map_cleared line 243
  35. theorem OAI.ExactFourier.Cascade.clearing_identity line 267
  36. theorem OAI.ExactFourier.Cascade.cell_clearing line 281
  37. def OAI.ExactFourier.PolynomialMatrix.bound line 302
  38. theorem OAI.ExactFourier.PolynomialMatrix.le_bound line 304
  39. def OAI.ExactFourier.PolynomialMatrix.Bounded line 313
  40. theorem OAI.ExactFourier.PolynomialMatrix.bounded_one line 315
  41. theorem OAI.ExactFourier.PolynomialMatrix.bounded_tensor line 320
  42. theorem OAI.ExactFourier.PolynomialMatrix.bounded_smul line 326
  43. theorem OAI.ExactFourier.PolynomialMatrix.bounded_power line 332
  44. theorem OAI.ExactFourier.Cascade.bounded_cleared line 344
  45. theorem OAI.ExactFourier.Cascade.exists_cleared_degree line 361