OAI/Analysis/Nuclearity/UnitizedCoefficientMaps.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Continuous linear maps realizing the finite coefficient formulas. For the abelian coefficient cone their complete positivity follows from the proved finite inner approximation, rather than an extra cone assumption.

  1. def OAI.WeakPureInfiniteness.unitizedRightOperator line 18
  2. def OAI.WeakPureInfiniteness.unitizedLeftOperator line 21
  3. lemma OAI.WeakPureInfiniteness.unitizedRightOperator_apply line 24
  4. lemma OAI.WeakPureInfiniteness.unitizedLeftOperator_apply line 27
  5. def OAI.WeakPureInfiniteness.unitizedCoefficientMap line 30
  6. lemma OAI.WeakPureInfiniteness.unitizedCoefficientMap_apply line 36
  7. lemma OAI.WeakPureInfiniteness.ApproximatelyOneStepAlong.approximatelyInner line 44
  8. theorem OAI.WeakPureInfiniteness.finiteUnitizedAbelianCoefficientCone_has_cp_map line 58