OAI/Computability/FourierCircuit/StreamSeries.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

The finite-coefficient meaning of the cell transfer H(z). The geometric resolvent is defined coefficientwise, without assumptions on D.

  1. def OAI.ExactFourier.CellSeries.resolvent line 13
  2. def OAI.ExactFourier.CellSeries.state line 15
  3. def OAI.ExactFourier.CellSeries.transfer line 17
  4. theorem OAI.ExactFourier.CellSeries.coeff_resolvent line 21
  5. theorem OAI.ExactFourier.CellSeries.coeff_state line 23
  6. theorem OAI.ExactFourier.CellSeries.coeff_transfer_zero line 27
  7. theorem OAI.ExactFourier.CellSeries.coeff_transfer_succ line 32
  8. theorem OAI.ExactFourier.CellSeries.constant_transfer line 38
  9. theorem OAI.ExactFourier.CellSeries.resolvent_right_inverse line 45
  10. theorem OAI.ExactFourier.CellSeries.resolvent_left_inverse line 58
  11. def OAI.ExactFourier.CellStream.run line 85
  12. theorem OAI.ExactFourier.CellStream.unit line 91
  13. theorem OAI.ExactFourier.CellStream.price line 97
  14. theorem OAI.ExactFourier.CellStream.fst_fst line 109
  15. theorem OAI.ExactFourier.CellStream.fst_succ line 112
  16. theorem OAI.ExactFourier.CellStream.succ_succ line 115
  17. theorem OAI.ExactFourier.CellStream.succ_fst line 119
  18. theorem OAI.ExactFourier.CellStream.fst_state line 123
  19. theorem OAI.ExactFourier.CellStream.succ_state line 126
  20. theorem OAI.ExactFourier.CellStream.state_entry line 131
  21. theorem OAI.ExactFourier.CellStream.state_block line 143
  22. theorem OAI.ExactFourier.CellStream.data_entry line 149
  23. theorem OAI.ExactFourier.CellStream.data_block line 163
  24. def OAI.ExactFourier.AxisJoin.rightOrder line 183
  25. abbrev OAI.ExactFourier.AxisJoin.join line 186
  26. theorem OAI.ExactFourier.AxisJoin.join_eq line 193
  27. theorem OAI.ExactFourier.AxisJoin.unit line 224
  28. theorem OAI.ExactFourier.AxisJoin.price line 230
  29. def OAI.ExactFourier.TimeLifts.rightEquiv line 258
  30. def OAI.ExactFourier.TimeLifts.timeSwap line 261
  31. def OAI.ExactFourier.TimeLifts.leftEquiv line 266
  32. def OAI.ExactFourier.TimeLifts.right line 270
  33. def OAI.ExactFourier.TimeLifts.left line 273
  34. theorem OAI.ExactFourier.TimeLifts.right_unit line 277
  35. theorem OAI.ExactFourier.TimeLifts.left_unit line 280
  36. theorem OAI.ExactFourier.TimeLifts.right_price line 283
  37. theorem OAI.ExactFourier.TimeLifts.left_price line 288
  38. theorem OAI.ExactFourier.TimeLifts.right_data line 294
  39. theorem OAI.ExactFourier.TimeLifts.left_data line 307
  40. theorem OAI.ExactFourier.TimeLifts.right_state line 320
  41. theorem OAI.ExactFourier.TimeLifts.left_state line 333
  42. abbrev OAI.ExactFourier.TensorAxis.Space line 358
  43. abbrev OAI.ExactFourier.TensorAxis.Fibers line 359
  44. def OAI.ExactFourier.TensorAxis.power line 364
  45. theorem OAI.ExactFourier.TensorAxis.card_space line 368
  46. theorem OAI.ExactFourier.TensorAxis.map_power line 373
  47. theorem OAI.ExactFourier.TensorAxis.mul_power line 385
  48. theorem OAI.ExactFourier.TensorAxis.power_one line 395
  49. theorem OAI.ExactFourier.TensorAxis.unit_power line 401
  50. theorem OAI.ExactFourier.TensorAxis.price_power line 406