OAI/LinearAlgebra/MatrixMultiplication/ComplexBounds/SquareBound.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Explicit complex square and rectangular matrix multiplication bounds.

  1. abbrev OAI.MatrixMultiplication.SquareBound.Coordinate line 19
  2. abbrev OAI.MatrixMultiplication.SquareBound.Carrier line 20
  3. def OAI.MatrixMultiplication.SquareBound.conditional line 22
  4. def OAI.MatrixMultiplication.SquareBound.program line 25
  5. theorem OAI.MatrixMultiplication.SquareBound.program_context line 31
  6. theorem OAI.MatrixMultiplication.SquareBound.program_view line 33
  7. theorem OAI.MatrixMultiplication.SquareBound.program_joint line 36
  8. def OAI.MatrixMultiplication.SquareBound.hierarchy line 44
  9. theorem OAI.MatrixMultiplication.SquareBound.hierarchy_complete line 47
  10. theorem OAI.MatrixMultiplication.SquareBound.hierarchy_x line 53
  11. theorem OAI.MatrixMultiplication.SquareBound.hierarchy_y line 54
  12. theorem OAI.MatrixMultiplication.SquareBound.hierarchy_z line 55
  13. theorem OAI.MatrixMultiplication.SquareBound.source_supported line 57
  14. theorem OAI.MatrixMultiplication.SquareBound.source_unit line 61
  15. def OAI.MatrixMultiplication.SquareBound.counts line 66
  16. theorem OAI.MatrixMultiplication.SquareBound.card_carrier line 68
  17. theorem OAI.MatrixMultiplication.SquareBound.total_counts line 71
  18. theorem OAI.MatrixMultiplication.SquareBound.total_counts_pos line 74
  19. theorem OAI.MatrixMultiplication.SquareBound.count_entropy line 78
  20. def OAI.MatrixMultiplication.SquareBound.family line 87
  21. theorem OAI.MatrixMultiplication.SquareBound.score_limit line 91
  22. theorem OAI.MatrixMultiplication.SquareBound.omega_lt_2267_div_1000 line 99
  23. theorem OAI.MatrixMultiplication.SquareBound.complex_omega_lt_2267_div_1000 line 104