OAI/Analysis/TriangularHilbert/WeightedStar.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularHilbert.MatrixEnergy.vertexRoot line 14
  2. def OAI.TriangularHilbert.MatrixEnergy.weightedArray line 17
  3. lemma OAI.TriangularHilbert.MatrixEnergy.vertexRoot_star line 21
  4. lemma OAI.TriangularHilbert.MatrixEnergy.vertexRoot_sq line 26
  5. lemma OAI.TriangularHilbert.MatrixEnergy.vertexRoot_commute_vertexProj line 33
  6. lemma OAI.TriangularHilbert.MatrixEnergy.triangle_weightedArray line 41
  7. lemma OAI.TriangularHilbert.MatrixEnergy.rowStar_weightedArray line 49
  8. lemma OAI.TriangularHilbert.MatrixEnergy.rowStar_apply line 56
  9. lemma OAI.TriangularHilbert.MatrixEnergy.rowStar_eq_blocks line 60
  10. def OAI.TriangularHilbert.MatrixEnergy.rowBare line 64
  11. def OAI.TriangularHilbert.MatrixEnergy.colBare line 67
  12. lemma OAI.TriangularHilbert.MatrixEnergy.starGram_weightedArray line 70
  13. lemma OAI.TriangularHilbert.MatrixEnergy.centerGram_weightedArray_padded line 82
  14. lemma OAI.TriangularHilbert.MatrixEnergy.rowBare_congr line 92
  15. lemma OAI.TriangularHilbert.MatrixEnergy.colBare_congr line 104
  16. lemma OAI.TriangularHilbert.MatrixEnergy.rowStar_mul_adjoint line 114