FiniteOperatorDuality.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite operator coefficient duality

The polar factor and a positive rank-one decomposition give vector coefficients whose two square sums are bounded by the functional norm. This is the finite-dimensional part of the commutant distance formula.

def OAI.KadisonKastler.finiteOperatorCoefficient line 23
Source documentation
A finite sum of vector coefficient functionals on bounded operators.
```
def finiteOperatorCoefficient {ι : Type*} [Fintype ι] (x y : ι → E) :
    (E →L[ℂ] E) →L[ℂ] ℂ :=
…
```
theorem OAI.KadisonKastler.finiteOperatorCoefficient_apply line 29
def OAI.KadisonKastler.operatorTracePairing line 38
Source documentation
The trace pairing is kept as a bounded functional so that its norm is the ordinary dual norm, with no additional trace-class definitions.
```
def operatorTracePairing (T : E →L[ℂ] E) : (E →L[ℂ] E) →L[ℂ] ℂ :=
…
```
theorem OAI.KadisonKastler.operatorTracePairing_apply line 44
theorem OAI.KadisonKastler.operatorTracePairing_rankOne line 47
theorem OAI.KadisonKastler.operatorTracePairing_sum line 53
theorem OAI.KadisonKastler.exists_finite_polar_coefficients line 60
theorem OAI.KadisonKastler.finite_dimensional_coefficient_factorization line 103