OAI/InformationTheory/DimensionTen/StateDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Normalization and product-free range of the dimension-ten Choi state.

  1. lemma OAI.DimensionTen.compositeChoi_trace_ne line 15
  2. lemma OAI.DimensionTen.compositeChoi_trace_nonneg line 18
  3. lemma OAI.DimensionTen.compositeChoi_trace_re line 21
  4. def OAI.DimensionTen.rho line 27
  5. lemma OAI.DimensionTen.rho_density line 30
  6. lemma OAI.DimensionTen.rho_productfree line 36
  7. lemma OAI.DimensionTen.operational_separable line 41
  8. lemma OAI.DimensionTen.rho_entangled line 47
  9. lemma OAI.DimensionTen.rho_range_contains_no_nonzero_product line 53
  10. theorem OAI.DimensionTen.main_state_geometry line 60