OAI/Probability/SKGap/Localization/Vectorize.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.ComplexMatrix.vectorize line 37
  2. lemma OAI.SKGap.ComplexMatrix.vectorize_norm line 42
  3. instance OAI.SKGap.ComplexMatrix.frobeniusInnerProduct line 49
  4. def OAI.SKGap.ComplexMatrix.hermitianBall line 58
  5. lemma OAI.SKGap.ComplexMatrix.hermitianBall_closed line 61
  6. lemma OAI.SKGap.ComplexMatrix.hermitianBall_convex line 66
  7. lemma OAI.SKGap.ComplexMatrix.hermitianBall_good line 81
  8. def OAI.SKGap.ComplexMatrix.matrixProject line 86
  9. lemma OAI.SKGap.ComplexMatrix.matrixProject_lipschitz line 89
  10. lemma OAI.SKGap.ComplexMatrix.matrixProject_bound line 93
  11. lemma OAI.SKGap.ComplexMatrix.matrixProject_eq_self line 97
  12. def OAI.SKGap.ComplexMatrix.truncatedG line 107
  13. lemma OAI.SKGap.ComplexMatrix.matrixProject_sub_norm line 111
  14. lemma OAI.SKGap.ComplexMatrix.truncatedG_opNorm line 115
  15. lemma OAI.SKGap.ComplexMatrix.truncatedG_sub_norm line 123
  16. lemma OAI.SKGap.ComplexMatrix.truncatedG_hermitian line 145
  17. lemma OAI.SKGap.ComplexMatrix.truncatedG_eq_inverse line 153
  18. def OAI.SKGap.ComplexMatrix.fl1 line 168
  19. def OAI.SKGap.ComplexMatrix.fl2 line 169
  20. lemma OAI.SKGap.ComplexMatrix.fl_nonneg line 170
  21. def OAI.SKGap.ComplexMatrix.diagonalChange line 176
  22. def OAI.SKGap.ComplexMatrix.shiftChange line 178
  23. def OAI.SKGap.ComplexMatrix.gBound line 180
  24. def OAI.SKGap.ComplexMatrix.gLip line 182
  25. def OAI.SKGap.ComplexMatrix.gChange line 184
  26. def OAI.SKGap.ComplexMatrix.gMixed line 186
  27. lemma OAI.SKGap.ComplexMatrix.diagonalChange_nonneg line 190
  28. lemma OAI.SKGap.ComplexMatrix.shiftChange_nonneg line 193
  29. lemma OAI.SKGap.ComplexMatrix.g_constants_nonneg line 197
  30. lemma OAI.SKGap.ComplexMatrix.truncatedG_parameter line 208
  31. lemma OAI.SKGap.ComplexMatrix.truncatedG_four_point line 240
  32. def OAI.SKGap.ComplexMatrix.truncatedK line 291
  33. def OAI.SKGap.ComplexMatrix.kBound line 295
  34. def OAI.SKGap.ComplexMatrix.kLip line 297
  35. def OAI.SKGap.ComplexMatrix.kMixed line 299
  36. lemma OAI.SKGap.ComplexMatrix.projected_sub_bound line 302
  37. lemma OAI.SKGap.ComplexMatrix.truncatedK_opNorm line 306
  38. lemma OAI.SKGap.ComplexMatrix.truncatedK_sub_norm line 315
  39. lemma OAI.SKGap.ComplexMatrix.truncatedK_four_point line 336