OAI/Analysis/KadisonSimilarity/Tracial/MatrixExpectationIdentification.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identification of finite matrix averaging with the constructed normal conditional expectation, for the relative quantization argument.

  1. def OAI.KadisonSimilarity.matrixSystemOfUnits line 15
  2. theorem OAI.KadisonSimilarity.matrix_average_eq_conditionalExpectation line 29
  3. theorem OAI.KadisonSimilarity.matrix_preGNS_norm_sq line 50
  4. theorem OAI.KadisonSimilarity.matrix_stage_energy_eq line 55