OAI/LinearAlgebra/MatrixMultiplication/ComplexBounds/CW75ReorderedFinite.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Explicit complex square and rectangular matrix multiplication bounds.

  1. def OAI.MatrixMultiplication.CW75ReorderedFinite.blocks line 18
  2. def OAI.MatrixMultiplication.CW75ReorderedFinite.copies line 20
  3. def OAI.MatrixMultiplication.CW75ReorderedFinite.rows line 23
  4. def OAI.MatrixMultiplication.CW75ReorderedFinite.inner line 24
  5. def OAI.MatrixMultiplication.CW75ReorderedFinite.columns line 25
  6. def OAI.MatrixMultiplication.CW75ReorderedFinite.rankBudget line 27
  7. def OAI.MatrixMultiplication.CW75ReorderedFinite.order line 30
  8. def OAI.MatrixMultiplication.CW75ReorderedFinite.degree line 34
  9. def OAI.MatrixMultiplication.CW75ReorderedFinite.sourceApproximation line 40
  10. def OAI.MatrixMultiplication.CW75ReorderedFinite.labelEquiv line 47
  11. def OAI.MatrixMultiplication.CW75ReorderedFinite.designatedX line 52
  12. def OAI.MatrixMultiplication.CW75ReorderedFinite.designatedY line 55
  13. def OAI.MatrixMultiplication.CW75ReorderedFinite.designatedZ line 58
  14. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.designated_coefficient_one line 61
  15. def OAI.MatrixMultiplication.CW75ReorderedFinite.leftSelect line 76
  16. def OAI.MatrixMultiplication.CW75ReorderedFinite.middleSelect line 82
  17. def OAI.MatrixMultiplication.CW75ReorderedFinite.rightSelect line 88
  18. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.selected_output line 94
  19. def OAI.MatrixMultiplication.CW75ReorderedFinite.approximation line 131
  20. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.dimensions_positive line 149
  21. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.volume_eq_copies line 153
  22. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.rows_pos line 157
  23. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.inner_pos line 160
  24. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.columns_pos line 163
  25. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.copies_pos line 166
  26. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.rankBudget_pos line 171
  27. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.dimensions_eq_pairingSize line 179
  28. theorem OAI.MatrixMultiplication.CW75ReorderedFinite.rank_power line 188