OAI/Analysis/BoundedHochschild/MatrixSystems.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Matrix systems, expectations and rational projection approximation.

  1. lemma OAI.HochschildMatrixSystems.projection_orthogonal_of_le_sub line 39
  2. lemma OAI.HochschildMatrixSystems.exists_partition_trace line 49
  3. structure OAI.HochschildMatrixSystems.MatrixSystem line 104
  4. lemma OAI.HochschildMatrixSystems.mul_of_initial_projection line 111
  5. theorem OAI.HochschildMatrixSystems.exists_matrixSystem line 124
  6. def OAI.HochschildMatrixSystems.MatrixSystem.expectation line 188
  7. lemma OAI.HochschildMatrixSystems.MatrixSystem.expectation_apply line 195
  8. lemma OAI.HochschildMatrixSystems.MatrixSystem.expectation_star line 198
  9. lemma OAI.HochschildMatrixSystems.MatrixSystem.entry_mul_expectation line 201
  10. lemma OAI.HochschildMatrixSystems.MatrixSystem.expectation_mul_entry line 210
  11. lemma OAI.HochschildMatrixSystems.MatrixSystem.commute_expectation line 216
  12. lemma OAI.HochschildMatrixSystems.MatrixSystem.expectation_eq_self line 220
  13. lemma OAI.HochschildMatrixSystems.MatrixSystem.expectation_idempotent line 232
  14. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_expectation line 238
  15. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_adjoint line 249
  16. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_residual_expectation line 260
  17. lemma OAI.HochschildMatrixSystems.MatrixSystem.norm_sq line 268
  18. lemma OAI.HochschildMatrixSystems.MatrixSystem.expectation_pythagoras line 273
  19. lemma OAI.HochschildMatrixSystems.MatrixSystem.expectation_gns_contract line 293
  20. lemma OAI.HochschildMatrixSystems.exists_matrixSystem_of_partition line 320
  21. lemma OAI.HochschildMatrixSystems.projection_trace_real line 372
  22. lemma OAI.HochschildMatrixSystems.exists_rational_subprojection line 378
  23. lemma OAI.HochschildMatrixSystems.exists_rational_partition line 412
  24. theorem OAI.HochschildMatrixSystems.exists_matrix_projection_approx line 461