OAI/Analysis/KadisonKastler/ConjugationComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Complete bounds for two operator conjugations

The smoothing operators need not be unitary. Their conjugation maps still have a complete comparison bound controlled by their norms and distance.

  1. def OAI.KadisonKastler.operatorConjugationLinear line 19
  2. theorem OAI.KadisonKastler.operatorConjugationLinear_apply line 25
  3. theorem OAI.KadisonKastler.complete_operatorConjugation_sub line 28