OAI/LinearAlgebra/MatrixMultiplication/Completion/ColorLaws.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. abbrev OAI.MatrixMultiplication.CompletionColorLaws.ColorSlice line 23
  2. def OAI.MatrixMultiplication.CompletionColorLaws.colorMix line 26
  3. theorem OAI.MatrixMultiplication.CompletionColorLaws.colorMix_mass line 37
  4. theorem OAI.MatrixMultiplication.CompletionColorLaws.colorMix_map_mass line 43
  5. theorem OAI.MatrixMultiplication.CompletionColorLaws.colorSlice_map_mass_zero line 63
  6. theorem OAI.MatrixMultiplication.CompletionColorLaws.colorMix_mass_zero line 73
  7. theorem OAI.MatrixMultiplication.CompletionColorLaws.colorMix_center_mass line 82
  8. theorem OAI.MatrixMultiplication.CompletionColorLaws.colorMix_output_mass line 91
  9. theorem OAI.MatrixMultiplication.CompletionColorLaws.exists_mass_pos line 100
  10. theorem OAI.MatrixMultiplication.CompletionColorLaws.colorMix_output_mass_pos line 110
  11. abbrev OAI.MatrixMultiplication.CompletionColorLaws.completionEvent line 120
  12. theorem OAI.MatrixMultiplication.CompletionColorLaws.completionEvent_constant line 126
  13. def OAI.MatrixMultiplication.CompletionColorLaws.iidColorLaw line 136
  14. theorem OAI.MatrixMultiplication.CompletionColorLaws.completionEvent_mass_pos line 143
  15. def OAI.MatrixMultiplication.CompletionColorLaws.conditionalCompletionLaw line 158
  16. theorem OAI.MatrixMultiplication.CompletionColorLaws.conditionalCompletionLaw_mass line 167