OAI/Analysis/OperatorAlgebra/AntiunitaryCPConjugation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Conjugating an operator-valued completely positive map on both sides by an involutive antiunitary preserves complete positivity. This is the operator calculation needed to transfer a commutant expectation across Tomita conjugation.

  1. def OAI.WeakPureInfiniteness.antiunitaryConjugate line 18
  2. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_apply line 26
  3. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_add line 30
  4. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_smul line 36
  5. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_involutive line 43
  6. lemma OAI.WeakPureInfiniteness.antiunitaryConjugate_norm_le line 50
  7. def OAI.WeakPureInfiniteness.antiunitaryMatrix line 56
  8. lemma OAI.WeakPureInfiniteness.antiunitaryMatrix_nonneg line 60
  9. def OAI.WeakPureInfiniteness.antiunitaryCPConjugate line 88
  10. lemma OAI.WeakPureInfiniteness.antiunitaryCPConjugate_norm_le line 100
  11. lemma OAI.WeakPureInfiniteness.antiunitaryCPConjugate_cp line 105