OAI/Analysis/FreeWords/MatrixConditionalExpectation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKMatrixExpectation.numericalHom line 18
  2. theorem OAI.KKMatrixExpectation.numericalHom_apply line 25
  3. def OAI.KKMatrixExpectation.matrixTraceMap line 28
  4. def OAI.KKMatrixExpectation.matrixExpectation line 31
  5. theorem OAI.KKMatrixExpectation.matrixExpectation_apply line 35
  6. theorem OAI.KKMatrixExpectation.matrixTraceMap_apply line 40
  7. theorem OAI.KKMatrixExpectation.trace_algebraMap line 45
  8. theorem OAI.KKMatrixExpectation.matrixTraceMap_numerical line 49
  9. theorem OAI.KKMatrixExpectation.matrixTraceMap_one line 54
  10. theorem OAI.KKMatrixExpectation.matrixExpectation_range line 60
  11. theorem OAI.KKMatrixExpectation.matrixExpectation_fix line 64
  12. theorem OAI.KKMatrixExpectation.matrixExpectation_right line 72
  13. theorem OAI.KKMatrixExpectation.matrixExpectation_trace line 85
  14. theorem OAI.KKMatrixExpectation.matrixTraceMap_faithful_numerical line 90
  15. theorem OAI.KKMatrixExpectation.matrix_scalar_amalgamated_cyclic_transport line 102