OAI/Analysis/Graph/Gradients.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Closed gradient subspaces of connected oriented multigraphs.

  1. structure OAI.SingerFour.OrientedGraph line 13
  2. inductive OAI.SingerFour.OrientedGraph.Walk line 21
  3. def OAI.SingerFour.OrientedGraph.Connected line 26
  4. def OAI.SingerFour.OrientedGraph.gradients line 28
  5. theorem OAI.SingerFour.OrientedGraph.mem_gradients line 47
  6. def OAI.SingerFour.OrientedGraph.Walk.integral line 50
  7. theorem OAI.SingerFour.OrientedGraph.Walk.integral_gradient line 55
  8. theorem OAI.SingerFour.OrientedGraph.eq_of_zero_differences line 69
  9. theorem OAI.SingerFour.OrientedGraph.potential_unique line 77
  10. theorem OAI.SingerFour.OrientedGraph.l2_eq_zero_of_constant line 90
  11. theorem OAI.SingerFour.OrientedGraph.l2_eq_zero_of_zero_differences line 102
  12. def OAI.SingerFour.OrientedGraph.normalizedPotential line 107
  13. theorem OAI.SingerFour.OrientedGraph.normalizedPotential_gradient line 111
  14. theorem OAI.SingerFour.OrientedGraph.mem_gradients_iff_normalized line 117
  15. theorem OAI.SingerFour.OrientedGraph.isClosed_gradients line 129
  16. theorem OAI.SingerFour.OrientedGraph.completeSpace_gradients line 145
  17. def OAI.SingerFour.OrientedGraph.finiteSupportGradients line 149
  18. def OAI.SingerFour.OrientedGraph.LocallyFinite line 167
  19. theorem OAI.SingerFour.OrientedGraph.hasFiniteSupport_differential line 170
  20. def OAI.SingerFour.OrientedGraph.finiteSupportDifferential line 187
  21. theorem OAI.SingerFour.OrientedGraph.finiteSupportDifferential_apply line 203
  22. theorem OAI.SingerFour.OrientedGraph.range_finiteSupportDifferential line 206
  23. def OAI.SingerFour.OrientedGraph.zeroBoundaryGradients line 218
  24. theorem OAI.SingerFour.OrientedGraph.finiteSupportGradients_le line 221
  25. theorem OAI.SingerFour.OrientedGraph.zeroBoundaryGradients_le line 225