OAI/Analysis/Nuclearity/PureProductFunctional.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Product pure-state functionals realized in the faithful product representation.

  1. def OAI.WeakPureInfiniteness.pureProductVector line 18
  2. theorem OAI.WeakPureInfiniteness.norm_pureProductVector line 23
  3. def OAI.WeakPureInfiniteness.pureProductCoefficient line 28
  4. theorem OAI.WeakPureInfiniteness.pureProductCoefficient_apply line 33
  5. theorem OAI.WeakPureInfiniteness.pureProductCoefficient_norm line 38
  6. theorem OAI.WeakPureInfiniteness.pureProductCoefficient_elementary line 49
  7. def OAI.WeakPureInfiniteness.faithfulPureProductFunctional line 68