OAI/Analysis/WeakInfiniteness/NuclearTensorMap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.tensorPolynomial line 31
  2. lemma OAI.WeakPureInfiniteness.tensorPolynomial_single line 34
  3. lemma OAI.WeakPureInfiniteness.tensorPolynomial_dense line 38
  4. lemma OAI.WeakPureInfiniteness.minimalTensor_clm_ext line 47
  5. def OAI.WeakPureInfiniteness.starHomContinuousLinear line 59
  6. def OAI.WeakPureInfiniteness.cpTensorPolynomial line 65
  7. lemma OAI.WeakPureInfiniteness.norm_cpTensorPolynomial_le line 68
  8. def OAI.WeakPureInfiniteness.minimalCPMap line 79
  9. lemma OAI.WeakPureInfiniteness.minimalCPMap_polynomial line 82
  10. lemma OAI.WeakPureInfiniteness.minimalCPMap_elementary line 86
  11. lemma OAI.WeakPureInfiniteness.norm_minimalCPMap_le line 91
  12. lemma OAI.WeakPureInfiniteness.minimalCPMap_kernel line 95
  13. lemma OAI.WeakPureInfiniteness.minimalCPMap_right_comm line 110