FiniteRowCochains.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Complete norm bounds for the finite cochain averages.

theorem OAI.KadisonKastler.finiteBilinearProduct_rowReplication_apply line 16
theorem OAI.KadisonKastler.finiteCochainAverage_matrix line 25
Source documentation
The cochain average at a matrix is a bilinear amplification followed by multiplication with the adjoint of the replicated row.
```
theorem finiteCochainAverage_matrix (r : κ → A) (f : A →ₗ[ℂ] A →ₗ[ℂ] A)
    (X : CStarMatrix τ ι A) :
    CStarMatrix.mapₗ (finiteCochainAverage r f) X =
      finiteBilinearProduct f X (rowReplication r) * (rowReplication r).conjTranspose := by
…
```
Mentions: OAI.KadisonKastler.finiteCochainAverage, OAI.KadisonKastler.finiteBilinearProduct, OAI.KadisonKastler.rowReplication

theorem OAI.KadisonKastler.HaagerupBound.finiteCochainAverage line 41

Source documentation

A normalized row produces a linear cochain with no loss of complete norm.

theorem HaagerupBound.finiteCochainAverage {f : A →ₗ[ℂ] A →ₗ[ℂ] A} {c : ℝ}
    (hf : HaagerupBound f c) (hc : 0 ≤ c)
    (r : κ → A) (hr : ∑ k, r k * star (r k) = 1) :
    CompletelyBoundedBy (finiteCochainAverage r f) c := by
…

Mentions: OAI.KadisonKastler.HaagerupBound, OAI.KadisonKastler.CompletelyBoundedBy