OAI/Probability/SKRatio/Matrices/Lin.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKRatioGaussian.ComplexMatrix.lin line 35
  2. def OAI.SKRatioGaussian.ComplexMatrix.opNorm line 36
  3. def OAI.SKRatioGaussian.ComplexMatrix.colVec line 37
  4. lemma OAI.SKRatioGaussian.ComplexMatrix.frobenius_sq line 39
  5. lemma OAI.SKRatioGaussian.ComplexMatrix.frobenius_col_sq line 45
  6. lemma OAI.SKRatioGaussian.ComplexMatrix.colVec_mul line 51
  7. lemma OAI.SKRatioGaussian.ComplexMatrix.lin_mul line 54
  8. lemma OAI.SKRatioGaussian.ComplexMatrix.lin_one line 60
  9. lemma OAI.SKRatioGaussian.ComplexMatrix.frobenius_mul_le_opNorm line 65
  10. lemma OAI.SKRatioGaussian.ComplexMatrix.lin_adjoint line 77
  11. lemma OAI.SKRatioGaussian.ComplexMatrix.opNorm_adjoint line 80
  12. lemma OAI.SKRatioGaussian.ComplexMatrix.frobenius_mul_le_opNorm_right line 84
  13. lemma OAI.SKRatioGaussian.ComplexMatrix.lin_unitary line 88
  14. lemma OAI.SKRatioGaussian.ComplexMatrix.frobenius_unitary_mul line 96
  15. lemma OAI.SKRatioGaussian.ComplexMatrix.frobenius_mul_unitary line 105