OAI/Analysis/Nuclearity/CommutantNullCone.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The finite GNS common-null cone and the Hahn--Banach conclusion of KR02 Lemma 7.18. Its elementary-span input is the application-specific consequence of Blackadar 3.3 / Tomiyama 5; it remains explicit here.

  1. def OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.nullCone line 32
  2. def OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.inclusionFunctional line 36
  3. def OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.elementarySpan line 40
  4. theorem OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.inclusionFunctional_mem_of_elementary_span line 49
  5. theorem OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.separating_sum_nonneg_of_elementary_span line 55
  6. theorem OAI.WeakPureInfiniteness.finite_coefficient_approximation_of_commutant_span line 82