OAI/Probability/SKGap/Localization/LinSub.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.ComplexMatrix.lin_sub line 31
  2. lemma OAI.SKGap.ComplexMatrix.lin_neg line 32
  3. lemma OAI.SKGap.ComplexMatrix.opNorm_smul line 33
  4. lemma OAI.SKGap.ComplexMatrix.unitary_exp_smul line 39
  5. lemma OAI.SKGap.ComplexMatrix.opNorm_exp_sub line 45
  6. lemma OAI.SKGap.ComplexMatrix.frobenius_exp_sub line 55
  7. lemma OAI.SKGap.ComplexMatrix.exp_four_point line 66
  8. lemma OAI.SKGap.ComplexMatrix.lin_csmul line 127
  9. lemma OAI.SKGap.ComplexMatrix.opNorm_csmul line 130
  10. def OAI.SKGap.ComplexMatrix.imaginary line 133
  11. lemma OAI.SKGap.ComplexMatrix.imaginary_skew line 137
  12. lemma OAI.SKGap.ComplexMatrix.imaginary_norm line 141
  13. lemma OAI.SKGap.ComplexMatrix.imaginary_opNorm line 144
  14. lemma OAI.SKGap.ComplexMatrix.imaginary_sub line 148
  15. lemma OAI.SKGap.ComplexMatrix.imaginary_exp_unitary line 151
  16. lemma OAI.SKGap.ComplexMatrix.imaginary_exp_norm line 155
  17. lemma OAI.SKGap.ComplexMatrix.imaginary_exp_opNorm_le line 159
  18. def OAI.SKGap.ComplexMatrix.kernelMatrix line 166
  19. lemma OAI.SKGap.ComplexMatrix.kernel_integrable line 169
  20. lemma OAI.SKGap.ComplexMatrix.kernelMatrix_lipschitz line 177
  21. lemma OAI.SKGap.ComplexMatrix.kernelMatrix_four_point line 194