OAI/Probability/SKGap/Localization/ExpDuhamel.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.exp_duhamel line 26
  2. lemma OAI.SKGap.exp_skew_unitary line 45
  3. lemma OAI.SKGap.exp_skew_difference line 51
  4. abbrev OAI.SKGap.ComplexMatrix.lin line 73
  5. def OAI.SKGap.ComplexMatrix.opNorm line 74
  6. def OAI.SKGap.ComplexMatrix.colVec line 75
  7. lemma OAI.SKGap.ComplexMatrix.frobenius_sq line 77
  8. lemma OAI.SKGap.ComplexMatrix.frobenius_col_sq line 83
  9. lemma OAI.SKGap.ComplexMatrix.colVec_mul line 89
  10. lemma OAI.SKGap.ComplexMatrix.lin_mul line 92
  11. lemma OAI.SKGap.ComplexMatrix.lin_one line 98
  12. lemma OAI.SKGap.ComplexMatrix.frobenius_mul_le_opNorm line 103
  13. lemma OAI.SKGap.ComplexMatrix.lin_adjoint line 115
  14. lemma OAI.SKGap.ComplexMatrix.opNorm_adjoint line 118
  15. lemma OAI.SKGap.ComplexMatrix.frobenius_mul_le_opNorm_right line 122
  16. lemma OAI.SKGap.ComplexMatrix.lin_unitary line 126
  17. lemma OAI.SKGap.ComplexMatrix.frobenius_unitary_mul line 134
  18. lemma OAI.SKGap.ComplexMatrix.frobenius_mul_unitary line 143
  19. def OAI.SKGap.ComplexMatrix.linEquiv line 154
  20. def OAI.SKGap.ComplexMatrix.linHom line 157
  21. lemma OAI.SKGap.ComplexMatrix.continuous_lin line 164
  22. lemma OAI.SKGap.ComplexMatrix.lin_exp line 167