OAI/Probability/SKRatio/Matrices/Fl1.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatioGaussian.ComplexMatrix.fl1 line 39
  2. def OAI.SKRatioGaussian.ComplexMatrix.fl2 line 40
  3. lemma OAI.SKRatioGaussian.ComplexMatrix.fl_nonneg line 41
  4. def OAI.SKRatioGaussian.ComplexMatrix.diagonalChange line 47
  5. def OAI.SKRatioGaussian.ComplexMatrix.shiftChange line 49
  6. def OAI.SKRatioGaussian.ComplexMatrix.gBound line 51
  7. def OAI.SKRatioGaussian.ComplexMatrix.gLip line 53
  8. def OAI.SKRatioGaussian.ComplexMatrix.gChange line 55
  9. def OAI.SKRatioGaussian.ComplexMatrix.gMixed line 57
  10. lemma OAI.SKRatioGaussian.ComplexMatrix.diagonalChange_nonneg line 61
  11. lemma OAI.SKRatioGaussian.ComplexMatrix.shiftChange_nonneg line 64
  12. lemma OAI.SKRatioGaussian.ComplexMatrix.g_constants_nonneg line 68
  13. lemma OAI.SKRatioGaussian.ComplexMatrix.truncatedG_parameter line 79
  14. lemma OAI.SKRatioGaussian.ComplexMatrix.truncatedG_four_point line 111
  15. def OAI.SKRatioGaussian.ComplexMatrix.truncatedK line 162
  16. def OAI.SKRatioGaussian.ComplexMatrix.kBound line 166
  17. def OAI.SKRatioGaussian.ComplexMatrix.kLip line 168
  18. def OAI.SKRatioGaussian.ComplexMatrix.kMixed line 170
  19. lemma OAI.SKRatioGaussian.ComplexMatrix.projected_sub_bound line 173
  20. lemma OAI.SKRatioGaussian.ComplexMatrix.truncatedK_opNorm line 177
  21. lemma OAI.SKRatioGaussian.ComplexMatrix.truncatedK_sub_norm line 186
  22. lemma OAI.SKRatioGaussian.ComplexMatrix.truncatedK_four_point line 207