OAI/Analysis/PureInfiniteness/SupportedTwoCopyMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A contractive two-copy map supported on one positive contraction. The support is enough; the initial relative isometries need not be central.

  1. def OAI.WeakPureInfiniteness.twoInnerMap line 16
  2. lemma OAI.WeakPureInfiniteness.twoInnerMap_apply line 20
  3. lemma OAI.WeakPureInfiniteness.twoInnerMap_cp line 23
  4. lemma OAI.WeakPureInfiniteness.twoInnerMap_norm_le_one line 29
  5. def OAI.WeakPureInfiniteness.supportedTwoCopyMap line 59
  6. lemma OAI.WeakPureInfiniteness.supportedTwoCopyMap_norm_le_one line 62
  7. lemma OAI.WeakPureInfiniteness.supportedTwoCopyMap_corner line 81