OAI/Analysis/Nuclearity/TensorCoefficientFunctional.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded finite coefficient functionals on the completed minimal tensor product. Their dependence on the coefficient vectors is continuous. This allows the cyclic-vector argument to handle arbitrary finite tensor tests.

  1. def OAI.WeakPureInfiniteness.operatorCoefficient line 19
  2. lemma OAI.WeakPureInfiniteness.operatorCoefficient_apply line 23
  3. def OAI.WeakPureInfiniteness.tensorCoefficientFunctional line 26
  4. lemma OAI.WeakPureInfiniteness.tensorCoefficientFunctional_apply line 34
  5. lemma OAI.WeakPureInfiniteness.tensorCoefficientFunctional_elementary line 42
  6. lemma OAI.WeakPureInfiniteness.tensorCoefficientFunctional_continuous line 53
  7. theorem OAI.WeakPureInfiniteness.finite_tensor_coefficient_approximation line 60