OAI/Analysis/TriangularHilbert/StarNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularHilbert.MatrixEnergy.rowNorm_rowStar line 13
2. lemma OAI.TriangularHilbert.MatrixEnergy.colNorm_rowStar line 17
3. lemma OAI.TriangularHilbert.MatrixEnergy.rowStar_norm_mono line 28
4. lemma OAI.TriangularHilbert.MatrixEnergy.weightedArray_norm line 39
5. lemma OAI.TriangularHilbert.MatrixEnergy.weightedArray_norm_sq line 44
6. lemma OAI.TriangularHilbert.MatrixEnergy.rowNorm_weightedStar_zero line 49
7. lemma OAI.TriangularHilbert.MatrixEnergy.colNorm_weightedStar_zero_one line 63
8. lemma OAI.TriangularHilbert.MatrixEnergy.rowNorm_weightedStar_one line 78
9. lemma OAI.TriangularHilbert.MatrixEnergy.colNorm_weightedStar_one_zero line 92