OAI/Analysis/PureInfiniteness/SupportedPairConstruction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The local relative Cuntz-pair construction. A single positive support gives noncentral orthogonal copies. One-step approximation of their supported two-copy map produces multiplicative local witnesses under the tensor-ideal elementary-span hypothesis.

  1. lemma OAI.WeakPureInfiniteness.norm_contractive_corner line 21
  2. theorem OAI.WeakPureInfiniteness.finite_relative_pair_of_elementary_span line 39
  3. theorem OAI.WeakPureInfiniteness.identityDiagonalization_of_elementary_span line 82
  4. theorem OAI.WeakPureInfiniteness.centralOInfinity_of_nuclear_and_elementary_span line 120