OAI/Analysis/OperatorAlgebra/IsometricCornerOperators.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Inclusion and compression of a closed Hilbert subspace transfer an expectation to represented projection corners.

  1. abbrev OAI.WeakPureInfiniteness.isometricCornerCompress line 17
  2. def OAI.WeakPureInfiniteness.isometricCornerLift line 22
  3. abbrev OAI.WeakPureInfiniteness.isometricCornerProjection line 25
  4. lemma OAI.WeakPureInfiniteness.isometricCorner_adjoint_apply line 28
  5. lemma OAI.WeakPureInfiniteness.isometricCornerCompress_apply line 32
  6. lemma OAI.WeakPureInfiniteness.isometricCornerLift_apply line 36
  7. lemma OAI.WeakPureInfiniteness.isometricCornerCompress_lift line 40
  8. lemma OAI.WeakPureInfiniteness.isometricCornerLift_injective line 46
  9. lemma OAI.WeakPureInfiniteness.isometricCornerLift_mul line 52
  10. lemma OAI.WeakPureInfiniteness.isometricCornerLift_star line 58
  11. def OAI.WeakPureInfiniteness.isometricCornerLiftHom line 65
  12. lemma OAI.WeakPureInfiniteness.isometricCornerProjection_apply line 74
  13. lemma OAI.WeakPureInfiniteness.isometricCornerProjection_inclusion line 77
  14. lemma OAI.WeakPureInfiniteness.isometricCornerProjection_isStarProjection line 81
  15. lemma OAI.WeakPureInfiniteness.isometricCornerLift_compress line 90
  16. lemma OAI.WeakPureInfiniteness.isometricCornerCompress_cp line 96
  17. lemma OAI.WeakPureInfiniteness.isometricCorner_inclusion_intertwines line 100
  18. lemma OAI.WeakPureInfiniteness.isometricCorner_adjoint_intertwines line 108
  19. lemma OAI.WeakPureInfiniteness.isometricCornerLift_mul_right line 117
  20. lemma OAI.WeakPureInfiniteness.isometricCornerLift_mul_left line 124
  21. lemma OAI.WeakPureInfiniteness.isometricCornerLift_commute_iff line 131
  22. lemma OAI.WeakPureInfiniteness.isometricCornerCompress_norm_le line 137
  23. def OAI.WeakPureInfiniteness.isometricCornerRestrictHom line 146