OAI/Analysis/TriangularHilbert/ZeroStar.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.MatrixEnergy.replaceZero line 14
2. lemma OAI.TriangularHilbert.MatrixEnergy.weightedArray_sub line 18
3. lemma OAI.TriangularHilbert.MatrixEnergy.rowStar_sub line 23
4. lemma OAI.TriangularHilbert.MatrixEnergy.replaceZero_sub line 33
5. lemma OAI.TriangularHilbert.MatrixEnergy.weightedArray_replaceZero_zero line 39
6. lemma OAI.TriangularHilbert.MatrixEnergy.rowStar_replaceZero_two line 47
7. lemma OAI.TriangularHilbert.MatrixEnergy.jump_sum_zero line 58
8. lemma OAI.TriangularHilbert.MatrixEnergy.jump_sum_one line 64
9. lemma OAI.TriangularHilbert.MatrixEnergy.weightedStar_replaceZero_norm_le line 73