OAI/Combinatorics/ThinTrees/GraphMatrix.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrongThinTree.qform line 14
  2. lemma OAI.StrongThinTree.qform_add line 16
  3. lemma OAI.StrongThinTree.qform_sub line 19
  4. lemma OAI.StrongThinTree.qform_smul line 22
  5. lemma OAI.StrongThinTree.qform_nonneg line 25
  6. lemma OAI.StrongThinTree.qform_mono line 28
  7. lemma OAI.StrongThinTree.qform_continuous line 33
  8. lemma OAI.StrongThinTree.qform_single line 36
  9. lemma OAI.StrongThinTree.posDef_of_le line 39
  10. def OAI.StrongThinTree.MultiGraph.laplacian line 44
  11. def OAI.StrongThinTree.MultiGraph.resistance line 45
  12. lemma OAI.StrongThinTree.MultiGraph.laplacian_psd line 46
  13. lemma OAI.StrongThinTree.MultiGraph.laplacian_qform line 50
  14. lemma OAI.StrongThinTree.MultiGraph.laplacian_cut line 58
  15. lemma OAI.StrongThinTree.MultiGraph.indicator_norm line 65
  16. def OAI.StrongThinTree.MultiGraph.baseMatrix line 69
  17. lemma OAI.StrongThinTree.MultiGraph.baseMatrix_pd line 70
  18. lemma OAI.StrongThinTree.MultiGraph.baseMatrix_cut line 72
  19. lemma OAI.StrongThinTree.MultiGraph.resistance_nonneg line 75
  20. lemma OAI.StrongThinTree.MultiGraph.resistance_antitone line 77