OAI/Probability/SKGap/Localization/RankCovariance.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.rankOneCovariance line 13
  2. def OAI.SKGap.rankOneCovarianceInverse line 16
  3. lemma OAI.SKGap.rankOneCovarianceInverse_mul line 19
  4. lemma OAI.SKGap.rankOneCovarianceInverse_mulVec line 31
  5. lemma OAI.SKGap.rankOneCovariance_posDef line 39
  6. lemma OAI.SKGap.rankOneCovariance_det line 57
  7. lemma OAI.SKGap.rankOneCovarianceInverse_quad line 67
  8. def OAI.SKGap.rankOneTransform line 96
  9. lemma OAI.SKGap.rankOneTransform_transpose line 100
  10. lemma OAI.SKGap.rankOneTransform_mul line 105
  11. lemma OAI.SKGap.rankOneTransform_det line 113
  12. lemma OAI.SKGap.rankOneTransform_inv line 121
  13. lemma OAI.SKGap.rankOneTransform_mulVec line 128
  14. lemma OAI.SKGap.rankOneTransform_norm_sq line 135