OAI/Analysis/TracialSplitting/KrausApproximation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NuclearTrace.trace_norm_mul_positive line 22
  2. lemma OAI.NuclearTrace.trace_norm_mul_selfAdjoint line 40
  3. def OAI.NuclearTrace.residualCoefficient line 61
  4. lemma OAI.NuclearTrace.residualCoefficient_synthesis line 63
  5. lemma OAI.NuclearTrace.residualCoefficient_mass line 70
  6. lemma OAI.NuclearTrace.residualCoefficient_pairing line 75
  7. def OAI.NuclearTrace.FiniteCoefficientSystem.mass line 91
  8. def OAI.NuclearTrace.FiniteCoefficientSystem.clip line 93
  9. def OAI.NuclearTrace.FiniteCoefficientSystem.residual line 96
  10. lemma OAI.NuclearTrace.FiniteCoefficientSystem.residual_nonneg line 99
  11. def OAI.NuclearTrace.FiniteCoefficientSystem.fill line 102
  12. def OAI.NuclearTrace.FiniteCoefficientSystem.normalize line 105
  13. lemma OAI.NuclearTrace.FiniteCoefficientSystem.output_one line 109
  14. lemma OAI.NuclearTrace.FiniteCoefficientSystem.normalize_output_one line 114
  15. lemma OAI.NuclearTrace.FiniteCoefficientSystem.normalize_pairing line 127
  16. lemma OAI.NuclearTrace.exists_clipping_tolerance line 153
  17. theorem OAI.NuclearTrace.nuclear_uniform_normalized_finite_approximation line 175