OAI/Analysis/WeakInfiniteness/PairUnitary.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.pairUnitary line 24
  2. def OAI.WeakPureInfiniteness.pairGroup line 27
  3. lemma OAI.WeakPureInfiniteness.pairGroup_of line 30
  4. lemma OAI.WeakPureInfiniteness.map_pairUnitary line 33
  5. lemma OAI.WeakPureInfiniteness.map_pairGroup line 51
  6. def OAI.WeakPureInfiniteness.logarithmContraction line 63
  7. lemma OAI.WeakPureInfiniteness.norm_logarithmContraction_le line 67
  8. lemma OAI.WeakPureInfiniteness.realPart_logarithmContraction line 81
  9. lemma OAI.WeakPureInfiniteness.imaginaryPart_logarithmContraction line 88
  10. lemma OAI.WeakPureInfiniteness.pairUnitary_logarithmContraction line 95