OAI/Probability/SKGap/Matrix/MatrixCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGap.MatrixCoordinates line 15
  2. def OAI.SKGap.goeMatrix line 19
  3. def OAI.SKGap.rawCoordinateMatrix line 24
  4. lemma OAI.SKGap.rawCoordinateMatrix_norm line 27
  5. lemma OAI.SKGap.goeMatrix_norm line 37
  6. lemma OAI.SKGap.goeMatrix_sub line 49
  7. lemma OAI.SKGap.goeMatrix_L2_lipschitz line 53
  8. lemma OAI.SKGap.goeMatrix_pi_lipschitz line 60
  9. def OAI.SKGap.symmetricElementary line 69
  10. lemma OAI.SKGap.goeMatrix_update line 73
  11. lemma OAI.SKGap.symmetricElementary_norm_le line 82
  12. lemma OAI.SKGap.goeMatrix_updated_hasDerivAt line 86