OAI/Analysis/Nuclearity/TensorFunctionalConjugation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite algebraic conjugation formula in KR02 Lemma 7.18. This is an identity for the constructed continuous positive tensor functional.

  1. lemma OAI.WeakPureInfiniteness.minimalTensor_sum_selfAdjoint line 19
  2. lemma OAI.WeakPureInfiniteness.commuting_operator_inner_split line 29
  3. lemma OAI.WeakPureInfiniteness.nuclearTensorFunctional_finite_conjugation line 40
  4. lemma OAI.WeakPureInfiniteness.nuclearTensorFunctional_finite_conjugation_vectors line 53