OAI/Analysis/KadisonSimilarity/Representation/FiniteOrbitComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite equal-square families have uniformly comparable orbit norms. The regularization stays inside the original C*-algebra.

  1. theorem OAI.KadisonSimilarity.exists_positive_shift_sqrt_unit line 15
  2. theorem OAI.KadisonSimilarity.unit_normalized_square_sum line 33
  3. theorem OAI.KadisonSimilarity.finite_equal_square_orbit_comparison line 48
  4. theorem OAI.KadisonSimilarity.listSquareSum_eq_sum_get line 114
  5. theorem OAI.KadisonSimilarity.listOrbitSum_eq_sum_get line 121
  6. theorem OAI.KadisonSimilarity.list_equal_square_orbit_comparison line 126