OAI/Analysis/KadisonKastler/NormalTracialSpatialSplit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.mem_of_fixed_commutant_unitaries line 17
2. theorem OAI.KadisonKastler.exists_selfAdjoint_split_of_normal_tracial_commutant line 43

   Source documentation

   The trace vector may live in a different faithful normal representation.

   theorem exists_selfAdjoint_split_of_normal_tracial_commutant
       (M : VonNeumannAlgebra H) (P : VonNeumannAlgebra J)
       (ρ : Algebra M.commutant ≃⋆ₐ[ℂ] Algebra P) (τ : TracialRepresentation P)
       (hρ : ∀ C : ℝ, Continuous (fun b : weakOperatorBall M.commutant C =>
         ofCLM (ρ ⟨b.val.toCLM, b.property.1⟩).val))
       (T : H →L[ℂ] H) (hTsa : IsSelfAdjoint T)
       (hT : ∀ a ∈ M, T * a - a * T ∈ M) :
       ∃ a : H →L[ℂ] H, a ∈ M ∧ IsSelfAdjoint a ∧ ‖a‖ ≤ ‖T‖ ∧
         T - a ∈ M.commutant := by
   …

   Mentions: OAI.KadisonKastler.Algebra