OAI/LinearAlgebra/MatrixMultiplication/Duality/WitnessRecurrence.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Dual matrix multiplication exponents and finite rectangular constructions.

  1. def OAI.MatrixMultiplication.DualWitness.massA line 11
  2. def OAI.MatrixMultiplication.DualWitness.massC line 12
  3. theorem OAI.MatrixMultiplication.DualWitness.massA_eq_massC line 14
  4. theorem OAI.MatrixMultiplication.DualWitness.massC_eq_massA line 19
  5. theorem OAI.MatrixMultiplication.DualWitness.minus_massA line 24
  6. theorem OAI.MatrixMultiplication.DualWitness.minus_massC line 30
  7. theorem OAI.MatrixMultiplication.DualWitness.minus_gap line 36
  8. theorem OAI.MatrixMultiplication.DualWitness.minus_gap_reverse line 42
  9. theorem OAI.MatrixMultiplication.DualWitness.plusA_massA line 48
  10. theorem OAI.MatrixMultiplication.DualWitness.plusC_massC line 55
  11. theorem OAI.MatrixMultiplication.DualWitness.log_exp_sum_pow_sub line 62
  12. theorem OAI.MatrixMultiplication.DualWitness.state4_hB line 76
  13. theorem OAI.MatrixMultiplication.DualWitness.state4_hA line 79
  14. theorem OAI.MatrixMultiplication.DualWitness.state4_hC line 82
  15. theorem OAI.MatrixMultiplication.DualWitness.state8_hB line 85
  16. theorem OAI.MatrixMultiplication.DualWitness.state8_hA line 90
  17. theorem OAI.MatrixMultiplication.DualWitness.state8_hC line 96
  18. theorem OAI.MatrixMultiplication.DualWitness.state8_hidden line 99
  19. theorem OAI.MatrixMultiplication.DualWitness.state8_gap line 103
  20. theorem OAI.MatrixMultiplication.DualWitness.state24_gap line 111
  21. theorem OAI.MatrixMultiplication.DualWitness.state48_gap line 117
  22. theorem OAI.MatrixMultiplication.DualWitness.state96_gap line 129
  23. theorem OAI.MatrixMultiplication.DualWitness.state288_gap line 134
  24. theorem OAI.MatrixMultiplication.DualWitness.initial_max line 146
  25. theorem OAI.MatrixMultiplication.DualWitness.state2_max line 149
  26. theorem OAI.MatrixMultiplication.DualWitness.state4_max line 152
  27. theorem OAI.MatrixMultiplication.DualWitness.state8_max line 157
  28. theorem OAI.MatrixMultiplication.DualWitness.state24_max line 162
  29. theorem OAI.MatrixMultiplication.DualWitness.state48_max line 166
  30. theorem OAI.MatrixMultiplication.DualWitness.state96_max line 170
  31. theorem OAI.MatrixMultiplication.DualWitness.state288_max line 174
  32. theorem OAI.MatrixMultiplication.DualWitness.state8_mass line 178
  33. theorem OAI.MatrixMultiplication.DualWitness.state24_mass line 184
  34. theorem OAI.MatrixMultiplication.DualWitness.state48_mass line 189
  35. theorem OAI.MatrixMultiplication.DualWitness.state96_mass line 197
  36. theorem OAI.MatrixMultiplication.DualWitness.state288_mass line 202
  37. theorem OAI.MatrixMultiplication.DualWitness.state288_normalizedHidden line 210