OAI/Analysis/KadisonKastler/TraceHullTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.trace_eq_of_mem_traceHull line 20

   Source documentation

   A trace value shared by every generator is shared by every algebra element in the trace Hilbert closure of their convex hull.

   theorem trace_eq_of_mem_traceHull (J : Algebra M →ₗ[ℂ] E)
       (hJ : ∀ x, ‖J x‖ = traceTwoNorm τ x)
       {S : Set (Algebra M)} {c : ℂ} (hS : ∀ x ∈ S, τ.toLinearMap x = c)
       {b : Algebra M} (hb : J b ∈ diagonalTraceHull J S) : τ.toLinearMap b = c := by
   …

   Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.diagonalTraceHull