OAI/Analysis/OperatorAlgebra/DensityQuadraticCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Passing the density-root trace identity through a common finite support, without finite-dimensionality of the represented Hilbert space.

  1. lemma OAI.WeakPureInfiniteness.tensorIsometry_compression line 19
  2. lemma OAI.WeakPureInfiniteness.finiteTensorDensity_compression line 42
  3. theorem OAI.WeakPureInfiniteness.densityRoot_left_quadratic line 59