OAI/Analysis/KadisonKastler/TraceUnitaryClosure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.star_mul_eq_one_of_trace_norm_one line 13
2. theorem OAI.KadisonKastler.mem_unitary_of_traceTwoNorm_eq_one line 36

   Source documentation

   A contraction attaining trace two-norm one is unitary.

   theorem mem_unitary_of_traceTwoNorm_eq_one
       (τ : FaithfulTracialState A) (a : A) (ha : ‖a‖ ≤ 1)
       (hτa : traceTwoNorm τ a = 1) : a ∈ unitary A := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.traceTwoNorm

3. theorem OAI.KadisonKastler.FiniteVectorTrace.isClosed_traceUnitary_image line 48

   Source documentation

   The unitary vectors form a closed subset of any faithful tracial Hilbert realization of a concrete finite algebra.

   theorem FiniteVectorTrace.isClosed_traceUnitary_image
       {τ : FaithfulTracialState (Algebra M)} (hτ : FiniteVectorTrace τ)
       (J : Algebra M →ₗ[ℂ] E) (hJ : ∀ a, ‖J a‖ = traceTwoNorm τ a) :
       IsClosed (J '' (unitary (Algebra M) : Set (Algebra M))) := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.traceTwoNorm