OAI/Analysis/KadisonSimilarity/Derivation/OrbitSquareNormalization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Upper and lower orbit estimates for a finite family whose sum of positive squares is one. This is the normalization step in the cyclic similarity argument.

  1. theorem OAI.KadisonSimilarity.normalized_adjoint_orbit_sum_le line 15
  2. theorem OAI.KadisonSimilarity.normalized_orbit_sum_le line 40
  3. theorem OAI.KadisonSimilarity.norm_sq_le_normalized_orbit_sum line 47