OAI/Analysis/Nuclearity/NuclearTensorFunctional.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The positive tensor functional of KR02 (7.14). It is obtained from the actual completely positive map and a commuting representation, using nuclearity for continuity in the minimal tensor norm.

  1. def OAI.WeakPureInfiniteness.nuclearTensorFunctional line 22
  2. lemma OAI.WeakPureInfiniteness.nuclearTensorFunctional_elementary line 33