OAI/Analysis/KadisonKastler/TracialSpatialGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.boundedSelfAdjointImplementers_midpoint line 19

   Source documentation

   Midpoints stay in the weakly compact family of implementers.

   theorem boundedSelfAdjointImplementers_midpoint (M : VonNeumannAlgebra H)
       (T : H →L[ℂ] H) {S V : H →WOT[ℂ] H}
       (hS : S ∈ boundedSelfAdjointImplementers M T)
       (hV : V ∈ boundedSelfAdjointImplementers M T) :
       (1 / 2 : ℝ) • (S + V) ∈ boundedSelfAdjointImplementers M T := by
   …

   Mentions: OAI.KadisonKastler.boundedSelfAdjointImplementers

2. theorem OAI.KadisonKastler.boundedSelfAdjointImplementers_conjugate line 40

   Source documentation

   Conjugation by a commutant unitary preserves every defining constraint.

   theorem boundedSelfAdjointImplementers_conjugate (M : VonNeumannAlgebra H)
       (T : H →L[ℂ] H) (hT : ∀ a ∈ M, T * a - a * T ∈ M)
       (u : unitary (H →L[ℂ] H)) (hu : u.val ∈ M.commutant)
       {S : H →L[ℂ] H} (hS : ofCLM S ∈ boundedSelfAdjointImplementers M T) :
       ofCLM (unitaryConj u S) ∈ boundedSelfAdjointImplementers M T := by
   …

   Mentions: OAI.KadisonKastler.boundedSelfAdjointImplementers, OAI.KadisonKastler.unitaryConj

3. theorem OAI.KadisonKastler.tracial_conjugation_difference_norm line 62

   Source documentation

   The trace metric on differences is preserved by commutant conjugation.

   theorem tracial_conjugation_difference_norm
       (N : VonNeumannAlgebra H) (τ : TracialRepresentation N)
       (u : unitary (Algebra N)) (S V : H →L[ℂ] H) (hSV : S - V ∈ N) :
       ‖(unitaryConj (ambientAlgebraUnitary u) S -
           unitaryConj (ambientAlgebraUnitary u) V) τ.vector‖ =
         ‖(S - V) τ.vector‖ := by
   …

   Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.unitaryConj, OAI.KadisonKastler.ambientAlgebraUnitary