OAI/Analysis/Triangular/Construction/L1Matrix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AtomicTriangular.L1Kernel.operator_apply line 9
2. def OAI.AtomicTriangular.MatrixBounds.l1Matrix line 22
3. lemma OAI.AtomicTriangular.MatrixBounds.l1Matrix_apply line 26
4. lemma OAI.AtomicTriangular.MatrixBounds.l1Matrix_norm line 32
5. lemma OAI.AtomicTriangular.MatrixBounds.l1Matrix_mul line 35
6. lemma OAI.AtomicTriangular.MatrixBounds.l1Matrix_one line 46
7. lemma OAI.AtomicTriangular.MatrixBounds.l1Matrix_add line 50
8. lemma OAI.AtomicTriangular.MatrixBounds.l1Matrix_sub line 54
9. lemma OAI.AtomicTriangular.MatrixBounds.l1Matrix_inverse line 57