OAI/Analysis/Nuclearity/RepresentedTensorFunctional.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite coefficient functional agrees with the positive tensor functional of the actual coefficient-enlarged map, on the full completion.

  1. def OAI.WeakPureInfiniteness.representedMap line 23
  2. lemma OAI.WeakPureInfiniteness.representedMap_cp line 26
  3. lemma OAI.WeakPureInfiniteness.representedMap_commute line 36
  4. def OAI.WeakPureInfiniteness.representedTensorFunctional line 40
  5. lemma OAI.WeakPureInfiniteness.representedTensorFunctional_elementary line 47
  6. lemma OAI.WeakPureInfiniteness.representedTensorFunctional_sum line 57
  7. theorem OAI.WeakPureInfiniteness.tensorCoefficientFunctional_unitized line 68