OAI/Analysis/BoundedHochschild/FactorCandidateCompactness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Compact sets of factorization operators whose coefficient maps take values in the original algebra. The range condition is retained explicitly.

  1. def OAI.BoundedHochschild.KadisonRingrose.representationWeakBall line 19
  2. def OAI.BoundedHochschild.KadisonRingrose.factorCandidates line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.factorCandidates_isClosed line 28
  4. theorem OAI.BoundedHochschild.KadisonRingrose.factorCandidates_isCompact line 37
  5. lemma OAI.BoundedHochschild.KadisonRingrose.weakFactorValue_norm_le line 44
  6. lemma OAI.BoundedHochschild.KadisonRingrose.mem_factorCandidates_of_range line 58
  7. theorem OAI.BoundedHochschild.KadisonRingrose.factorCandidates_realize line 74
  8. theorem OAI.BoundedHochschild.KadisonRingrose.factorCandidates_invariant line 99