OAI/Analysis/KadisonKastler/FiniteHaagerupBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite index changes for bilinear amplifications.

  1. def OAI.KadisonKastler.finiteBilinearProduct line 16

    Source documentation

    The bilinear amplification with arbitrary finite index types.

    def finiteBilinearProduct (f : A →ₗ[ℂ] A →ₗ[ℂ] A)
    {ι κ τ : Type*} [Fintype κ] (X : CStarMatrix ι κ A) (Y : CStarMatrix κ τ A) :
    CStarMatrix ι τ A := CStarMatrix.ofMatrix fun i j => ∑ k, f (X i k) (Y k j)
…
  2. theorem OAI.KadisonKastler.finiteBilinearProduct_reindex line 21
  3. theorem OAI.KadisonKastler.HaagerupBound.finite line 35