OAI/LinearAlgebra/MatrixMultiplication/Completion/EntropyAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. def OAI.MatrixMultiplication.CompletionEntropyAlgebra.binaryEntropy line 14
  2. def OAI.MatrixMultiplication.CompletionEntropyAlgebra.conditionalMixEntropy line 16
  3. theorem OAI.MatrixMultiplication.CompletionEntropyAlgebra.conditionalMixEntropy_eq_split line 20
  4. theorem OAI.MatrixMultiplication.CompletionEntropyAlgebra.conditionalMixEntropy_cancel line 30
  5. theorem OAI.MatrixMultiplication.CompletionEntropyAlgebra.ratio_range line 44
  6. theorem OAI.MatrixMultiplication.CompletionEntropyAlgebra.ratio_complement line 49
  7. theorem OAI.MatrixMultiplication.CompletionEntropyAlgebra.binaryEntropy_cardinal_mixture line 54
  8. theorem OAI.MatrixMultiplication.CompletionEntropyAlgebra.conditionalMixEntropy_incident line 70
  9. theorem OAI.MatrixMultiplication.CompletionEntropyAlgebra.conditionalMixEntropy_gibbs line 102