OAI/Analysis/OperatorAlgebra/TracialSpatialState.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The spatial diagonal state in the finite tracial injectivity argument. The finite-vector argument follows Anantharaman--Delaroche, Pacific J. Math. 171 (1995), Lemma 3.7 and Proposition 3.6, pp. 328--330.

  1. lemma OAI.WeakPureInfiniteness.tracial_spatial_state_extend line 17
  2. theorem OAI.WeakPureInfiniteness.expectation_tracial_spatial_state line 44

    Source documentation

    The trace diagonal is realized by an actual spatial state.

    theorem expectation_tracial_spatial_state (M : VonNeumannAlgebra H)
    [PartialOrder M.toStarSubalgebra] [StarOrderedRing M.toStarSubalgebra]
    (τ : Pureness.TracialState M.toStarSubalgebra)
    (E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hE : CompletelyPositive E) (hEr : ∀ T, E T ∈ M)
    (hEf : ∀ T, T ∈ M → E T = T) :
    ∃ φ : (NuclearUltrapower.HilbertSchmidt H →L[ℂ]
        NuclearUltrapower.HilbertSchmidt H) →ₚ[ℂ] ℂ,
      φ 1 = 1 ∧ ∀ a b : M.toStarSubalgebra,
        φ (densityLeftRepresentation (a : H →L[ℂ] H) *
          densityRightRepresentation (MulOpposite.op (b : H →L[ℂ] H))) =
            τ.functional (a * b) := by
…

    Mentions: OAI.Pureness.TracialState, OAI.WeakPureInfiniteness.CompletelyPositive, OAI.NuclearUltrapower.HilbertSchmidt, OAI.WeakPureInfiniteness.densityLeftRepresentation, OAI.WeakPureInfiniteness.densityRightRepresentation