OAI/LinearAlgebra/MatrixMultiplication/Duality/WitnessRealization.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. theorem OAI.MatrixMultiplication.DualWitnessRealization.program_context line 19
  2. theorem OAI.MatrixMultiplication.DualWitnessRealization.program_joint line 22
  3. def OAI.MatrixMultiplication.DualWitnessRealization.hierarchy line 31
  4. theorem OAI.MatrixMultiplication.DualWitnessRealization.hierarchy_complete line 35
  5. theorem OAI.MatrixMultiplication.DualWitnessRealization.hierarchy_x line 40
  6. theorem OAI.MatrixMultiplication.DualWitnessRealization.hierarchy_y line 41
  7. theorem OAI.MatrixMultiplication.DualWitnessRealization.hierarchy_z line 42
  8. def OAI.MatrixMultiplication.DualWitnessRealization.tensor line 44
  9. def OAI.MatrixMultiplication.DualWitnessRealization.retainedLeafEquiv line 47
  10. def OAI.MatrixMultiplication.DualWitnessRealization.approximation line 51
  11. theorem OAI.MatrixMultiplication.DualWitnessRealization.base_unit line 56
  12. theorem OAI.MatrixMultiplication.DualWitnessRealization.tensor_unit_coefficients line 63
  13. theorem OAI.MatrixMultiplication.DualWitnessRealization.source_supported line 72
  14. theorem OAI.MatrixMultiplication.DualWitnessRealization.source_unit line 76
  15. def OAI.MatrixMultiplication.DualWitnessRealization.witness line 80
  16. theorem OAI.MatrixMultiplication.DualWitnessRealization.witness_rank line 85
  17. theorem OAI.MatrixMultiplication.DualWitnessRealization.source_log line 91
  18. theorem OAI.MatrixMultiplication.DualWitnessRealization.source_log_positive line 95