OAI/Analysis/KadisonKastler/CornerHomogeneityApplication.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact corner specialization of state homogeneity

Connes--Størmer, J. Funct. Anal. 28 (1978), 187--196, states norm transitivity of inner automorphisms on faithful normal states of a type III₁ factor. Its vector-state special case gives the corner application formalized here.

  1. def OAI.KadisonKastler.FaithfulVectorStateHomogeneity line 21
  2. theorem OAI.KadisonKastler.vectorCornerState_supported line 28
  3. theorem OAI.KadisonKastler.TypeIIIFactor.corner_comparison_of_vector_state_homogeneity line 40