OAI/Analysis/KadisonKastler/ConstructedComparisonNormalizerAlignment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

From comparison normalizers to a common action

Multiplying the selected normalizer of V(g) U(g)* by U(g) produces a normalizer close to the actual representation V. The choices need no regularity; the invariant-mean correction supplies one conjugating unitary.

  1. theorem OAI.KadisonKastler.constructed_norm_comparison_normalizer_error line 20
  2. theorem OAI.KadisonKastler.constructed_exists_common_action_of_comparison_normalizers line 30