OAI/Analysis/KadisonKastler/TwoCornerHomogeneity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

State homogeneity with a fixed centralizing projection

The two normalized corner comparisons combine to a unitary commuting with the original projection, under the vector-state specialization of Connes--Størmer homogeneity.

  1. theorem OAI.KadisonKastler.sandwichFunctional_real_smul line 21
  2. theorem OAI.KadisonKastler.vectorCornerState_sandwich line 26
  3. theorem OAI.KadisonKastler.TypeIIIFactor.central_projection_state_comparison line 36