OAI/Analysis/PureInfiniteness/ApproximatelyInnerCP.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A point-norm limit of finite inner compressions is completely positive. This gives positivity for the actual finite coefficient cone used in KR02.

  1. lemma OAI.WeakPureInfiniteness.ApproximatelyInnerAlong.completelyPositive line 17