OAI/Analysis/OperatorAlgebra/TracialMinimalMultiplication.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Extension of the finite tracial multiplication representation to the actual minimal tensor product.

  1. lemma OAI.WeakPureInfiniteness.tracialMinimalAlgebraic_mul line 17
  2. lemma OAI.WeakPureInfiniteness.tracialMinimalAlgebraic_star line 30
  3. lemma OAI.WeakPureInfiniteness.tracialMinimalMultiplication_norm_le line 45
  4. def OAI.WeakPureInfiniteness.tracialMinimalMultiplication line 54

    Source documentation

    The finite tracial amenability representation, constructed from the expectation by the existing minimal tensor extension theorem.

    def tracialMinimalMultiplication :
    MinimalTensor M.toStarSubalgebra M.toStarSubalgebraᵐᵒᵖ →⋆ₙₐ[ℂ]
      (τ.functional.GNS →L[ℂ] τ.functional.GNS) :=
…

    Mentions: OAI.WeakPureInfiniteness.MinimalTensor

  5. lemma OAI.WeakPureInfiniteness.tracialMinimalMultiplication_algebraic line 60
  6. lemma OAI.WeakPureInfiniteness.tracialMinimalMultiplication_elementary line 67