OAI/Analysis/TracialSplitting/PartitionCoupling.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.traceOneNorm_covariance_l2 line 19
  2. lemma OAI.CurrentMain.traceOneNorm_covariance_sum_l2 line 51
  3. lemma OAI.CurrentMain.global_partition_covariance_l2 line 82
  4. lemma OAI.CurrentMain.choi_sqrt_factorization line 145
  5. lemma OAI.CurrentMain.choi_bistochastic_family line 156
  6. def OAI.CurrentMain.scalarMatrixUnit line 181
  7. lemma OAI.CurrentMain.star_scalarMatrixUnit line 185
  8. lemma OAI.CurrentMain.scalarMatrixUnit_mul line 190
  9. lemma OAI.CurrentMain.sum_scalarMatrixUnit_diag line 199
  10. lemma OAI.CurrentMain.matrixUnits_positive line 208
  11. lemma OAI.CurrentMain.cp_choi_positive line 223
  12. lemma OAI.CurrentMain.ucp_choi_bistochastic line 227
  13. lemma OAI.CurrentMain.scalarMatrixUnit_expansion line 236
  14. lemma OAI.CurrentMain.linearMap_choi_expansion line 245
  15. lemma OAI.CurrentMain.scalar_contraction_dilation line 251
  16. def OAI.CurrentMain.scalarMix line 274
  17. lemma OAI.CurrentMain.scalarMix_covariance line 278
  18. lemma OAI.CurrentMain.scalarMix_covariance_of_isometry line 299
  19. lemma OAI.CurrentMain.scalarMix_dilation_covariance line 306
  20. lemma OAI.CurrentMain.choi_evaluation line 330
  21. lemma OAI.CurrentMain.choi_coupling line 354
  22. lemma OAI.CurrentMain.trace_choi_coupling_error line 400
  23. lemma OAI.CurrentMain.choi_global_partition_bound line 426
  24. lemma OAI.CurrentMain.ucp_global_partition_averaging line 443
  25. lemma OAI.CurrentMain.trace_choi_coupling_pairing line 460
  26. lemma OAI.CurrentMain.choi_global_partition_pairing line 478
  27. lemma OAI.CurrentMain.normalized_choi_global_averaging line 494