OAI/Analysis/KadisonKastler/ConjugateFiniteThreshold.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite spectral cuts and the conjugate right action

  1. theorem OAI.KadisonKastler.conjugationOperator_finsetSum line 19
  2. theorem OAI.KadisonKastler.conjugationOperator_real_sum line 26
  3. theorem OAI.KadisonKastler.conjugationOperator_finiteThreshold line 37
  4. theorem OAI.KadisonKastler.finiteSpectralCut_integral_le line 43