OAI/Analysis/KadisonKastler/ModularHaagerupWitnesses.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The quantitative Haagerup premise from constructed modular data

The uniform constant is six. This is the sufficient condition appearing in AHHM, arXiv:1804.05706v2, Theorem 7.2, specialized to a fixed faithful cyclic vector. The implication to scalar bicentralizers is not assumed here.

  1. def OAI.KadisonKastler.HaagerupCommutatorWitnesses line 22
  2. theorem OAI.KadisonKastler.haagerupCommutatorWitnesses_of_modular_product line 29