NuclearCommutantExpectation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A nuclear algebra in any Hilbert-space representation has a cpc projection onto its commutant. This is the forward, commutant part of Lance's injectivity argument: extend the commuting tensor representation and use its multiplicative domain. No converse from injectivity to nuclearity is asserted here.

theorem OAI.WeakPureInfiniteness.nuclear_representation_commutant_expectation line 25
Source documentation
A cpc retraction of all bounded operators onto the commutant of any representation of a nuclear C*-algebra.
```
theorem nuclear_representation_commutant_expectation (hA : Nuclear A)
    (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) :
    ∃ P : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H), CompletelyPositive P ∧ ‖P‖ ≤ 1 ∧
      (∀ T, P T ∈ representationCommutant π) ∧
      (∀ T, T ∈ representationCommutant π → P T = T) := by
…
```
Mentions: OAI.WeakPureInfiniteness.Nuclear, OAI.WeakPureInfiniteness.CompletelyPositive, OAI.WeakPureInfiniteness.representationCommutant