OAI/Analysis/TriangularHilbert/InitialAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.MatrixEnergy.hsSquare line 13
2. def OAI.TriangularHilbert.MatrixEnergy.hsCube line 15
3. lemma OAI.TriangularHilbert.MatrixEnergy.hsSquare_nonneg line 17
4. lemma OAI.TriangularHilbert.MatrixEnergy.hsSquare_star line 20
5. lemma OAI.TriangularHilbert.MatrixEnergy.hsSquare_rowStar_sum line 25
6. lemma OAI.TriangularHilbert.MatrixEnergy.hsSquare_zero line 37
7. lemma OAI.TriangularHilbert.MatrixEnergy.hsSquare_rowStar line 39
8. lemma OAI.TriangularHilbert.MatrixEnergy.cubic_add_le line 45
9. lemma OAI.TriangularHilbert.MatrixEnergy.energy_star_le_hsCube line 55
10. lemma OAI.TriangularHilbert.MatrixEnergy.hsSquare_weightedArray line 62
11. lemma OAI.TriangularHilbert.MatrixEnergy.hsCube_weightedArray_le line 74