OAI/Probability/SpanningForest/GraphFreeKernel.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Problem336.FreeKernel.complete_closedGraphCycleSpace line 15
  2. instance OAI.Problem336.FreeKernel.projection_closedGraphCycleSpace line 20
  3. def OAI.Problem336.FreeKernel.finiteKernel line 24
  4. def OAI.Problem336.FreeKernel.graphKernel line 27
  5. theorem OAI.Problem336.FreeKernel.cycle_projection_tendsto line 30
  6. theorem OAI.Problem336.FreeKernel.finiteKernel_tendsto line 38
  7. theorem OAI.Problem336.FreeKernel.finiteKernel_inner_tendsto line 44
  8. theorem OAI.Problem336.FreeKernel.finiteKernel_minor_tendsto line 50
  9. def OAI.Problem336.FreeKernel.edgeVector line 60
  10. def OAI.Problem336.FreeKernel.kernelEntry line 62
  11. theorem OAI.Problem336.FreeKernel.finiteKernel_edge_minor_tendsto line 65
  12. def OAI.Problem336.FreeKernel.finiteInclusionMinor line 73
  13. def OAI.Problem336.FreeKernel.inclusionMinorLimit line 77
  14. theorem OAI.Problem336.FreeKernel.finiteInclusionMinor_tendsto line 80
  15. theorem OAI.Problem336.FreeKernel.common_inclusion_limits_of_finite_identity line 88
  16. theorem OAI.Problem336.FreeKernel.finiteCycle_le_supported line 97
  17. theorem OAI.Problem336.FreeKernel.finiteKernel_mem_supported line 106
  18. theorem OAI.Problem336.FreeKernel.finiteKernel_inner_edge_eq_zero_of_not_mem line 112
  19. theorem OAI.Problem336.FreeKernel.graphCycle_le_supported line 120
  20. theorem OAI.Problem336.FreeKernel.graphKernel_mem_supported line 130
  21. theorem OAI.Problem336.FreeKernel.kernelEntry_eq_zero_of_not_adj line 136