OAI/Analysis/KadisonKastler/SpatialStateCentrality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

State-central sequences in the first tensor leg

The product-state commutator is bounded by the original state commutator. Thus bicentralizer membership of a first-leg operator implies membership in the original algebra. Together with the independent-swap argument, this is the needed product-leg specialization of AHHM, Proposition7.1.

  1. def OAI.KadisonKastler.spatialLeftAlgebraHom line 25
  2. theorem OAI.KadisonKastler.spatialLeftAlgebraHom_val line 30
  3. theorem OAI.KadisonKastler.spatialLeftAlgebraHom_tensorVector line 34
  4. theorem OAI.KadisonKastler.tensorVectorSlice_mul_left line 39
  5. theorem OAI.KadisonKastler.tensorVectorSlice_mul_right line 46
  6. theorem OAI.KadisonKastler.spatialLeft_stateCommutator_apply line 55
  7. theorem OAI.KadisonKastler.spatialLeft_stateCommutator_norm_le line 66
  8. theorem OAI.KadisonKastler.stateBicentralizerMember_spatialLeft_pullback line 79
  9. theorem OAI.KadisonKastler.spatial_bicentralizer_mem_left_bicentralizer line 105