OAI/Analysis/OperatorAlgebra/IsometricCornerExpectation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A concrete cpc retraction onto a von Neumann algebra restricts to a concrete cpc retraction onto each represented projection corner.

  1. lemma OAI.WeakPureInfiniteness.isometricCorner_commutant_commutes line 21
  2. def OAI.WeakPureInfiniteness.isometricCornerCommutantHom line 27
  3. def OAI.WeakPureInfiniteness.isometricCornerVonNeumann line 33
  4. lemma OAI.WeakPureInfiniteness.isometricCornerVonNeumann_mem_iff line 37
  5. lemma OAI.WeakPureInfiniteness.isometricCornerCompress_mem line 57
  6. def OAI.WeakPureInfiniteness.isometricCornerExpectation line 63
  7. lemma OAI.WeakPureInfiniteness.isometricCornerExpectation_cp line 69
  8. lemma OAI.WeakPureInfiniteness.isometricCornerExpectation_norm_le line 76
  9. lemma OAI.WeakPureInfiniteness.isometricCornerExpectation_mem line 87
  10. lemma OAI.WeakPureInfiniteness.isometricCornerExpectation_fixed line 94