OAI/Analysis/OperatorAlgebra/DensityRootTrace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The left spatial vector functional of a density root is the original finite positive functional. The finite-dimensional computation is the trace identity used before passage to a common finite support.

  1. lemma OAI.WeakPureInfiniteness.finiteOperatorTensor_left line 17
  2. lemma OAI.WeakPureInfiniteness.densityRoot_eq_finiteOperatorTensor line 25
  3. lemma OAI.WeakPureInfiniteness.densityRoot_left_quadratic_finite line 33