OAI/Analysis/KadisonKastler/LocalizedFactorNorm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The norm of a right factor localized by an operator in the original commutant is constant on a minimal row family.

  1. theorem OAI.KadisonKastler.isClosed_weakRectangularBall line 20
  2. theorem OAI.KadisonKastler.isClosed_localized_factor_norm line 32
  3. theorem OAI.KadisonKastler.representationRowAverage_comp_commutant line 41
  4. theorem OAI.KadisonKastler.minimal_row_family_localized_factor_norm line 55