OAI/LinearAlgebra/MatrixMultiplication/Completion/FiniteRealization.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.power_coefficient_one line 18
  2. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.complete_coefficient_one line 26
  3. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.script_coefficient_one line 36
  4. def OAI.MatrixMultiplication.CompletionFiniteRealization.scriptSourceApproximation line 43
  5. def OAI.MatrixMultiplication.CompletionFiniteRealization.blocks line 55
  6. def OAI.MatrixMultiplication.CompletionFiniteRealization.copies line 57
  7. def OAI.MatrixMultiplication.CompletionFiniteRealization.rows line 59
  8. def OAI.MatrixMultiplication.CompletionFiniteRealization.inner line 60
  9. def OAI.MatrixMultiplication.CompletionFiniteRealization.columns line 61
  10. def OAI.MatrixMultiplication.CompletionFiniteRealization.order line 63
  11. def OAI.MatrixMultiplication.CompletionFiniteRealization.degree line 67
  12. def OAI.MatrixMultiplication.CompletionFiniteRealization.labelEquiv line 73
  13. def OAI.MatrixMultiplication.CompletionFiniteRealization.designatedX line 78
  14. def OAI.MatrixMultiplication.CompletionFiniteRealization.designatedY line 81
  15. def OAI.MatrixMultiplication.CompletionFiniteRealization.designatedZ line 84
  16. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.leading_shape line 87
  17. def OAI.MatrixMultiplication.CompletionFiniteRealization.leftSelect line 102
  18. def OAI.MatrixMultiplication.CompletionFiniteRealization.middleSelect line 108
  19. def OAI.MatrixMultiplication.CompletionFiniteRealization.rightSelect line 114
  20. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.designated_coefficient_one line 120
  21. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.selected_output line 129
  22. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.dimensions_positive line 162
  23. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.volume_eq_copies line 167
  24. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.copies_pos line 172
  25. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.auxiliaryRank_pos line 177
  26. def OAI.MatrixMultiplication.CompletionFiniteRealization.sourceApproximation line 185
  27. def OAI.MatrixMultiplication.CompletionFiniteRealization.approximation line 191
  28. def OAI.MatrixMultiplication.CompletionFiniteRealization.realization line 214
  29. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.realization_occurrences line 244
  30. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.realization_multiplicity line 248
  31. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.realization_auxiliaryRank line 252
  32. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.realization_rows line 257
  33. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.realization_inner line 261
  34. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.realization_columns line 265
  35. theorem OAI.MatrixMultiplication.CompletionFiniteRealization.realization_volume line 269