OAI/Computability/FourierCircuit/PivotAlgebra.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.Pivot.matrix line 9
  2. theorem OAI.ExactFourier.Pivot.factor line 13
  3. theorem OAI.ExactFourier.Pivot.unit line 19
  4. theorem OAI.ExactFourier.Pivot.solve line 26
  5. theorem OAI.ExactFourier.Pivot.involutive line 33
  6. theorem OAI.ExactFourier.Pivot.schur_unit line 43
  7. theorem OAI.ExactFourier.MatrixPrice.pair_le_two_of_entry line 57
  8. theorem OAI.ExactFourier.MatrixPrice.pair_le_two line 84
  9. def OAI.ExactFourier.twoProdEquiv line 110
  10. def OAI.ExactFourier.pairLayer line 116
  11. theorem OAI.ExactFourier.pairLayer_eq line 119
  12. theorem OAI.ExactFourier.pairLayer_unit line 125
  13. theorem OAI.ExactFourier.MatrixPrice.pair_layer line 130
  14. theorem OAI.ExactFourier.exists_invertible_evaluation line 146
  15. def OAI.ExactFourier.Pivot.side line 177
  16. theorem OAI.ExactFourier.Pivot.side_eq line 181
  17. theorem OAI.ExactFourier.Pivot.side_unit line 190
  18. theorem OAI.ExactFourier.Pivot.side_price line 194
  19. def OAI.ExactFourier.Pivot.middle line 200
  20. theorem OAI.ExactFourier.Pivot.middle_eq line 205
  21. def OAI.ExactFourier.Pivot.P line 213
  22. def OAI.ExactFourier.Pivot.Q line 214
  23. theorem OAI.ExactFourier.Pivot.P_unit line 216
  24. theorem OAI.ExactFourier.Pivot.Q_unit line 220
  25. def OAI.ExactFourier.Pivot.data line 225
  26. def OAI.ExactFourier.Pivot.co line 228
  27. def OAI.ExactFourier.Pivot.bo line 230
  28. def OAI.ExactFourier.Pivot.state line 232
  29. def OAI.ExactFourier.Pivot.cell line 233
  30. theorem OAI.ExactFourier.Pivot.cell_eq line 237
  31. theorem OAI.ExactFourier.Pivot.cell_unit line 260
  32. theorem OAI.ExactFourier.Pivot.cell_price line 267
  33. theorem OAI.ExactFourier.Pivot.choose_data line 285
  34. theorem OAI.ExactFourier.Pivot.denominator line 303
  35. theorem OAI.ExactFourier.Pivot.cell_feedback line 307
  36. theorem OAI.ExactFourier.MatrixPrice.pivot_bound line 332