ColumnRowEstimates.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite row and column estimates inside a properly infinite algebra.

def OAI.BoundedHochschild.KadisonRingrose.columnRow line 18
Source documentation
A row, realized inside the algebra by orthogonal isometries.
```
def columnRow (x : Fin n → M) : M := ∑ i, x i * star (c i : M)
```
def OAI.BoundedHochschild.KadisonRingrose.columnColumn line 21
Source documentation
A column, realized inside the algebra by orthogonal isometries.
```
def columnColumn (y : Fin n → M) : M := ∑ i, (c i : M) * y i
…
```
lemma OAI.BoundedHochschild.KadisonRingrose.columnRow_mul_column line 24
lemma OAI.BoundedHochschild.KadisonRingrose.columnRow_mul_star line 40
lemma OAI.BoundedHochschild.KadisonRingrose.star_column_mul_column line 47
lemma OAI.BoundedHochschild.KadisonRingrose.columnRow_norm_sq line 54
lemma OAI.BoundedHochschild.KadisonRingrose.columnColumn_norm_sq line 59
lemma OAI.BoundedHochschild.KadisonRingrose.finite_row_column_estimate line 66
Source documentation
The finite row-column inequality, using only the particular isometries available in the properly infinite case.
```
lemma finite_row_column_estimate (x y : Fin n → M) :
    ‖∑ i, x i * y i‖ ^ 2 ≤ ‖∑ i, x i * star (x i)‖ * ‖∑ i, star (y i) * y i‖ := by
…
```