OAI/LinearAlgebra/MatrixMultiplication/Duality/WitnessArithmetic.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. structure OAI.MatrixMultiplication.DualWitness.State line 13
  2. def OAI.MatrixMultiplication.DualWitness.initial line 20
  3. def OAI.MatrixMultiplication.DualWitness.minus line 22
  4. def OAI.MatrixMultiplication.DualWitness.plusA line 32
  5. def OAI.MatrixMultiplication.DualWitness.plusC line 40
  6. def OAI.MatrixMultiplication.DualWitness.state2 line 48
  7. def OAI.MatrixMultiplication.DualWitness.state4 line 49
  8. def OAI.MatrixMultiplication.DualWitness.state8 line 50
  9. def OAI.MatrixMultiplication.DualWitness.state24 line 51
  10. def OAI.MatrixMultiplication.DualWitness.state48 line 52
  11. def OAI.MatrixMultiplication.DualWitness.state96 line 53
  12. def OAI.MatrixMultiplication.DualWitness.state288 line 54
  13. def OAI.MatrixMultiplication.DualWitness.normalizedHidden line 56
  14. def OAI.MatrixMultiplication.DualWitness.rho8 line 59
  15. def OAI.MatrixMultiplication.DualWitness.rho24 line 60
  16. def OAI.MatrixMultiplication.DualWitness.delta24 line 61
  17. def OAI.MatrixMultiplication.DualWitness.z48 line 62
  18. def OAI.MatrixMultiplication.DualWitness.rho48 line 63
  19. def OAI.MatrixMultiplication.DualWitness.rho96 line 64
  20. def OAI.MatrixMultiplication.DualWitness.delta96 line 65
  21. def OAI.MatrixMultiplication.DualWitness.rho288 line 66
  22. def OAI.MatrixMultiplication.DualWitness.z288 line 67
  23. def OAI.MatrixMultiplication.DualWitness.hiddenRate line 68
  24. def OAI.MatrixMultiplication.DualWitness.aspect line 70
  25. theorem OAI.MatrixMultiplication.DualWitness.state_factors line 72
  26. theorem OAI.MatrixMultiplication.DualWitness.state8_rho line 76
  27. theorem OAI.MatrixMultiplication.DualWitness.state24_rho line 79
  28. theorem OAI.MatrixMultiplication.DualWitness.state48_rho line 82
  29. theorem OAI.MatrixMultiplication.DualWitness.state96_rho line 85
  30. theorem OAI.MatrixMultiplication.DualWitness.state288_rho line 88
  31. theorem OAI.MatrixMultiplication.DualWitness.rho8_range line 91
  32. theorem OAI.MatrixMultiplication.DualWitness.rho24_range line 92
  33. theorem OAI.MatrixMultiplication.DualWitness.rho48_range line 93
  34. theorem OAI.MatrixMultiplication.DualWitness.rho96_range line 94
  35. theorem OAI.MatrixMultiplication.DualWitness.rho288_range line 95