OAI/Analysis/TracialSplitting/ConditionalSplitting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.familyTwoNorm_le_uniform line 25
  2. lemma OAI.CurrentMain.familyHalvingError_le_uniform line 30
  3. theorem OAI.CurrentMain.rr_central_splitting_from_diagonals line 50
  4. lemma OAI.CurrentMain.continuous_tensorPair line 91
  5. lemma OAI.CurrentMain.compact_unitary_of_finiteDimensional line 98
  6. def OAI.CurrentMain.diagonalTestCoordinate line 108
  7. lemma OAI.CurrentMain.diagonalTestCoordinate_apply line 114
  8. lemma OAI.CurrentMain.diagonalTestAtom_unitary_sum line 119
  9. theorem OAI.CurrentMain.diagonalDualBound_of_compactUnitary line 136
  10. theorem OAI.CurrentMain.positiveDiagonal_of_finiteDimensional line 191