OAI/Analysis/Triangular/Auxiliary/MatrixNorm.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.MatrixBounds.colNorm line 8
  2. def OAI.AtomicTriangular.MatrixBounds.matNorm line 9
  3. lemma OAI.AtomicTriangular.MatrixBounds.colNorm_nonneg line 15
  4. lemma OAI.AtomicTriangular.MatrixBounds.colNorm_le_matNorm line 17
  5. lemma OAI.AtomicTriangular.MatrixBounds.matNorm_nonneg line 21
  6. lemma OAI.AtomicTriangular.MatrixBounds.matNorm_le line 24
  7. lemma OAI.AtomicTriangular.MatrixBounds.colNorm_add line 29
  8. lemma OAI.AtomicTriangular.MatrixBounds.matNorm_add line 34
  9. lemma OAI.AtomicTriangular.MatrixBounds.colNorm_neg line 40
  10. lemma OAI.AtomicTriangular.MatrixBounds.matNorm_neg line 42
  11. lemma OAI.AtomicTriangular.MatrixBounds.matNorm_sub line 44
  12. lemma OAI.AtomicTriangular.MatrixBounds.colNorm_mul line 48
  13. lemma OAI.AtomicTriangular.MatrixBounds.matNorm_mul line 60
  14. lemma OAI.AtomicTriangular.MatrixBounds.matNorm_one line 66
  15. lemma OAI.AtomicTriangular.MatrixBounds.matNorm_pow line 77
  16. lemma OAI.AtomicTriangular.MatrixBounds.norm_of_inverse_residual line 85
  17. lemma OAI.AtomicTriangular.MatrixBounds.inverse_residual_approx line 112
  18. def OAI.AtomicTriangular.MatrixBounds.vecNorm line 132
  19. lemma OAI.AtomicTriangular.MatrixBounds.vecNorm_nonneg line 134
  20. lemma OAI.AtomicTriangular.MatrixBounds.vecNorm_zero_iff line 136
  21. lemma OAI.AtomicTriangular.MatrixBounds.matrix_vecNorm line 145
  22. lemma OAI.AtomicTriangular.MatrixBounds.isUnit_of_residual line 155
  23. lemma OAI.AtomicTriangular.MatrixBounds.inverse_bound_of_residual line 168
  24. lemma OAI.AtomicTriangular.MatrixBounds.inverse_error_of_residual line 185