FiniteNormalTrace.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Normal traces in finite von Neumann algebras

Ringrose, Theorem 5.4: the compact convex unitary orbit of a positive normal functional contains a normal trace with the same values on the center. This construction assumes no scalar or center-valued trace.

lemma OAI.BoundedHochschild.KadisonRingrose.tracial_of_unitary_invariant line 28

theorem OAI.BoundedHochschild.KadisonRingrose.exists_normal_tracial_average line 48

Source documentation

Every positive normal functional on a finite von Neumann algebra has a normal tracial average agreeing with it on the center.

theorem exists_normal_tracial_average (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (ψ : M →ₚ[ℂ] ℂ) (hψ : TraceInPredual e ψ) :
    ∃ τ : M →ₚ[ℂ] ℂ, TraceInPredual e τ ∧ τ 1 = ψ 1 ∧
      (∀ a b : M, τ (a * b) = τ (b * a)) ∧
      ∀ a : M, (∀ b : M, a * b = b * a) → τ a = ψ a := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra, OAI.BoundedHochschild.TraceInPredual