OAI/Analysis/KadisonKastler/RegularTensorConjugation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.pull_commutant line 15
2. theorem OAI.KadisonKastler.constant_conjugation line 32
3. theorem OAI.KadisonKastler.conjugate_tensor_mem line 40
4. theorem OAI.KadisonKastler.Conjugates.regularTensor line 59
5. theorem OAI.KadisonKastler.norm_regularConstantUnitary_sub_one line 75
6. theorem OAI.KadisonKastler.kkDistance_regularTensor_conjugate_le line 84

   Source documentation

   Moving a factor by u costs at most twice the displacement in the regular tensor gap, just as it does in the original representation.

   theorem kkDistance_regularTensor_conjugate_le (M N : VonNeumannAlgebra H)
       (u : unitary (H →L[ℂ] H)) :
       kkDistance (regularTensorAlgebra N) (regularTensorAlgebra (unitaryConjugateAlgebra u M)) ≤
         kkDistance (regularTensorAlgebra N) (regularTensorAlgebra M) +
           2 * ‖(u : H →L[ℂ] H) - 1‖ := by
   …

   Mentions: OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.regularTensorAlgebra, OAI.KadisonKastler.unitaryConjugateAlgebra