OAI/Probability/SpanningForest/ReducedLaplacian.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.ReducedLaplacian.EdgeAdj line 11
  2. def OAI.Problem336.ReducedLaplacian.Connected line 14
  3. theorem OAI.Problem336.ReducedLaplacian.potential_eq_of_connected line 17
  4. def OAI.Problem336.ReducedLaplacian.extendZero line 30
  5. theorem OAI.Problem336.ReducedLaplacian.extendZero_root line 33
  6. theorem OAI.Problem336.ReducedLaplacian.extendZero_subtype line 36
  7. def OAI.Problem336.ReducedLaplacian.reducedGradient line 40
  8. lemma OAI.Problem336.ReducedLaplacian.sum_indicator_mul line 46
  9. theorem OAI.Problem336.ReducedLaplacian.reducedGradient_mulVec line 65
  10. theorem OAI.Problem336.ReducedLaplacian.reducedGradient_mulVec_injective line 72
  11. def OAI.Problem336.ReducedLaplacian.weightedLaplacian line 91
  12. theorem OAI.Problem336.ReducedLaplacian.weightedLaplacian_posDef line 95
  13. theorem OAI.Problem336.ReducedLaplacian.weightedLaplacian_isUnit line 103
  14. theorem OAI.Problem336.ReducedLaplacian.weightedLaplacian_det_ne_zero line 108