OAI/Probability/FreeIsing/Trees/PathCylinders.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ConnectedHull.prefix_length_eq line 12
  2. theorem OAI.Problem367.ConnectedHull.mem_vertices line 16
  3. theorem OAI.Problem367.ConnectedHull.prefix_mem_vertices line 26
  4. theorem OAI.Problem367.ConnectedHull.connected_vertices line 30
  5. def OAI.Problem367.ConnectedHull.path line 41
  6. theorem OAI.Problem367.ConnectedHull.path_injective line 44
  7. def OAI.Problem367.ConnectedHull.pathEdge line 51
  8. theorem OAI.Problem367.ConnectedHull.pathEdge_injective line 54
  9. theorem OAI.Problem367.ConnectedHull.vertices_eq_image_path line 60
  10. theorem OAI.Problem367.ConnectedHull.inducedEdges_vertices line 71
  11. theorem OAI.Problem367.ConnectedHull.freeCylinderWeight_vertices line 107
  12. def OAI.Problem367.ConnectedHull.pathAssignment line 118
  13. theorem OAI.Problem367.ConnectedHull.pathAssignment_path line 122
  14. theorem OAI.Problem367.ConnectedHull.path_cylinder_eq line 129
  15. theorem OAI.Problem367.ConnectedHull.freeLaw_path_cylinder line 145
  16. theorem OAI.Problem367.ConnectedHull.path_zero line 158
  17. theorem OAI.Problem367.ConnectedHull.path_last line 161
  18. theorem OAI.Problem367.ConnectedHull.chain_product_nonneg line 164
  19. def OAI.Problem367.AlternatingPath.word line 174
  20. theorem OAI.Problem367.AlternatingPath.word_length line 178
  21. theorem OAI.Problem367.AlternatingPath.word_isChain line 184
  22. def OAI.Problem367.AlternatingPath.vertex line 194
  23. theorem OAI.Problem367.AlternatingPath.vertex_length line 199
  24. theorem OAI.Problem367.exists_treeVertex_length line 204