OAI/Analysis/KadisonSimilarity/Representation/StrongApplyLimits.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded strong convergence can be applied to converging vectors. Only the contractive case needed for spectral projections is used.

  1. theorem OAI.KadisonSimilarity.contractive_strong_zero_apply line 15
  2. theorem OAI.KadisonSimilarity.contractive_complement_apply line 33