OAI/Analysis/Nuclearity/ProductStateIdealExcision.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The excision part of the elementary-ideal theorem: a product pure state which detects a kernel element detects a positive elementary kernel element. The separate nuclear ideal-separation step is not assumed here.

  1. lemma OAI.WeakPureInfiniteness.norm_sandwich_contraction line 24
  2. theorem OAI.WeakPureInfiniteness.pure_product_detects_elementary_kernel line 33
  3. theorem OAI.WeakPureInfiniteness.pure_product_vanishes_on_kernel line 113