OAI/LinearAlgebra/MatrixMultiplication/Completion/Conditioning.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. theorem OAI.MatrixMultiplication.CompletionLaws.sum_subtype_indicator line 17
  2. def OAI.MatrixMultiplication.CompletionLaws.eventMass line 22
  3. theorem OAI.MatrixMultiplication.CompletionLaws.eventMass_nonneg line 25
  4. def OAI.MatrixMultiplication.CompletionLaws.condition line 28
  5. theorem OAI.MatrixMultiplication.CompletionLaws.condition_mass line 34
  6. theorem OAI.MatrixMultiplication.CompletionLaws.condition_coordinate_mass line 38
  7. theorem OAI.MatrixMultiplication.CompletionLaws.eventMass_coordinate line 66
  8. def OAI.MatrixMultiplication.CompletionLaws.transport line 87
  9. theorem OAI.MatrixMultiplication.CompletionLaws.transport_mass line 90
  10. theorem OAI.MatrixMultiplication.CompletionLaws.transport_entropy line 93