OAI/Analysis/OperatorAlgebra/TracialSpatialMultiplication.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite tracial multiplication representation is continuous for the spatial tensor norm when the represented von Neumann algebra admits a c.p. expectation.

  1. def OAI.WeakPureInfiniteness.subalgebraOppositeHom line 17
  2. def OAI.WeakPureInfiniteness.tracialSpatialTensor line 22
  3. lemma OAI.WeakPureInfiniteness.tracialSpatialTensor_tmul line 30
  4. def OAI.WeakPureInfiniteness.tracialMultiplicationTensor line 40
  5. lemma OAI.WeakPureInfiniteness.tracialMultiplicationTensor_vector line 45
  6. lemma OAI.WeakPureInfiniteness.tracialMultiplicationTensor_cyclic line 51
  7. lemma OAI.WeakPureInfiniteness.tracial_multiplication_norm_le_of_state line 56
  8. theorem OAI.WeakPureInfiniteness.tracial_multiplication_norm_le line 75

    Source documentation

    The finite tracial part of the injectivity/semidiscreteness argument: the diagonal multiplication representation is bounded by the spatial norm.

    theorem tracial_multiplication_norm_le
    (E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hE : CompletelyPositive E) (hEr : ∀ T, E T ∈ M)
    (hEf : ∀ T, T ∈ M → E T = T)
    (z : M.toStarSubalgebra ⊗[ℂ] M.toStarSubalgebraᵐᵒᵖ) :
    ‖tracialMultiplicationTensor M τ z‖ ≤ ‖tracialSpatialTensor M z‖ := by
…

    Mentions: OAI.WeakPureInfiniteness.CompletelyPositive, OAI.WeakPureInfiniteness.tracialMultiplicationTensor, OAI.WeakPureInfiniteness.tracialSpatialTensor