OAI/Computability/FourierCircuit/MonomialFeedback.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ExactFourier.MatrixPrice.one_add_monomial line 10
  2. theorem OAI.ExactFourier.MatrixPrice.source_shear line 44
  3. theorem OAI.ExactFourier.DensePair.four_price line 63
  4. def OAI.ExactFourier.DensePair.rowY line 106
  5. def OAI.ExactFourier.DensePair.rowX line 111
  6. def OAI.ExactFourier.DensePair.delta line 116
  7. def OAI.ExactFourier.DensePair.signs line 117
  8. def OAI.ExactFourier.DensePair.rankOne line 118
  9. def OAI.ExactFourier.DensePair.scaled line 120
  10. def OAI.ExactFourier.DensePair.scaled2 line 122
  11. def OAI.ExactFourier.DensePair.B line 124
  12. theorem OAI.ExactFourier.DensePair.rankOne_mul line 126
  13. def OAI.ExactFourier.DensePair.left1 line 136
  14. theorem OAI.ExactFourier.DensePair.left1_ne line 138
  15. theorem OAI.ExactFourier.DensePair.signs_ne line 142
  16. theorem OAI.ExactFourier.DensePair.scale1 line 144
  17. def OAI.ExactFourier.DensePair.left2 line 152
  18. def OAI.ExactFourier.DensePair.right2 line 153
  19. theorem OAI.ExactFourier.DensePair.left2_ne line 154
  20. theorem OAI.ExactFourier.DensePair.right2_ne line 156
  21. theorem OAI.ExactFourier.DensePair.scale2 line 159
  22. def OAI.ExactFourier.DensePair.bitsRow line 165
  23. def OAI.ExactFourier.DensePair.bitsCol line 171
  24. theorem OAI.ExactFourier.DensePair.tensor_scaled line 177
  25. theorem OAI.ExactFourier.DensePair.B_unit line 181
  26. theorem OAI.ExactFourier.DensePair.rankOne_price line 195
  27. theorem OAI.ExactFourier.DensePair.normalized_price line 213
  28. theorem OAI.ExactFourier.DensePair.price line 238
  29. abbrev OAI.ExactFourier.Embedded.complement line 273
  30. instance OAI.ExactFourier.Embedded.(instance at line 274) line 274
  31. instance OAI.ExactFourier.Embedded.(instance at line 275) line 275
  32. def OAI.ExactFourier.Embedded.coordinates line 277
  33. theorem OAI.ExactFourier.Embedded.coordinates_inl line 282
  34. theorem OAI.ExactFourier.Embedded.coordinates_inr line 284
  35. def OAI.ExactFourier.Embedded.matrix line 287
  36. theorem OAI.ExactFourier.Embedded.unit line 290
  37. theorem OAI.ExactFourier.Embedded.price line 293
  38. def OAI.ExactFourier.Embedded.pair line 297
  39. theorem OAI.ExactFourier.Embedded.pair_zero line 301
  40. theorem OAI.ExactFourier.Embedded.pair_one line 303
  41. theorem OAI.ExactFourier.Embedded.complement_ne_pair line 306
  42. theorem OAI.ExactFourier.Embedded.pair_matrix line 312
  43. theorem OAI.ExactFourier.Embedded.pair_price line 334