OAI/Analysis/KadisonKastler/CenteredTestCommutatorWitness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The commutator inequalities furnished by the centered test

This gives the quantitative premise used by the Haagerup criterion in AHHM, arXiv:1804.05706v2, Theorem 7.2, with the uniform constant six. The implication from that criterion to scalar bicentralizers is separate.

  1. theorem OAI.KadisonKastler.energy_gap line 20
  2. theorem OAI.KadisonKastler.centeredTest_commutator_witness line 26