AdjointCommutators.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The adjoint version of a scalar corner estimate, used in propagation.

theorem OAI.KadisonSimilarity.commutator_adjoint_left line 14
Source documentation
Taking adjoints exchanges the two commutator factors and changes the sign.
```
theorem commutator_adjoint_left (Y X : H →L[ℂ] H) :
    commutator (star Y) X = -star (commutator Y (star X)) := by
…
```
Mentions: OAI.KadisonSimilarity.commutator
theorem OAI.KadisonSimilarity.norm_commutator_adjoint_left line 18
theorem OAI.KadisonSimilarity.scalarCommutatorNorm_adjoint line 25
Source documentation
A scalar commutator estimate on a star algebra also holds for the adjoint operator, with precisely the same constant.
```
theorem scalarCommutatorNorm_adjoint (P : VonNeumannAlgebra H) (Y : H →L[ℂ] H) :
    scalarCommutatorNorm P (star Y) = scalarCommutatorNorm P Y := by
…
```
Mentions: OAI.KadisonSimilarity.scalarCommutatorNorm