OAI/LinearAlgebra/MatrixMultiplication/Completion/Laws.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. def OAI.MatrixMultiplication.CompletionLaws.mixture line 16
  2. theorem OAI.MatrixMultiplication.CompletionLaws.mixture_mass line 19
  3. theorem OAI.MatrixMultiplication.CompletionLaws.mixture_map_mass line 24
  4. theorem OAI.MatrixMultiplication.CompletionLaws.mixture_common_marginal line 45
  5. theorem OAI.MatrixMultiplication.CompletionLaws.joint_common_marginal line 53
  6. theorem OAI.MatrixMultiplication.CompletionLaws.common_marginal_entropy line 76
  7. theorem OAI.MatrixMultiplication.CompletionLaws.independent_entropy line 85