OAI/Analysis/KadisonKastler/CommonRepresentationGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The fiber gap from nearby norm-separable test algebras

The common representation is contractive even when it is not faithful. Exact contraction lifting to each source algebra then preserves their ordinary gap. Kaplansky density passes the estimate to the fiber algebras.

  1. theorem OAI.KadisonKastler.commonRepresentation_unitBall_approx line 22
  2. theorem OAI.KadisonKastler.kkDistance_commonRepresentation_le line 51