OAI/Analysis/KadisonKastler/TypeIIIConstantNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Type III corners of a constant-norm convex family vanish

The nonzero corner can be made strictly positive by independent small left and right contractions. Both contractions come from convex unitary averages. Removing the resulting off-diagonal corner then contradicts the constant norm of the family.

  1. theorem OAI.KadisonKastler.CuntzFamily.upperRight_eq_zero_of_typeIII_constantNorm_of_projection_countability line 32
  2. theorem OAI.KadisonKastler.CuntzFamily.upperRight_eq_zero_of_typeIII_constantNorm line 62