OAI/Probability/FreeIsing/Trees/EdgeIIDLaw.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem367.EdgeIIDLaw.rowMeasure line 15
  2. abbrev OAI.Problem367.EdgeIIDLaw.edgeMeasure line 18
  3. def OAI.Problem367.EdgeIIDLaw.codingMeasure line 21
  4. theorem OAI.Problem367.EdgeIIDLaw.measurePreserving_priority_edgeLabels line 25
  5. theorem OAI.Problem367.EdgeIIDLaw.measurePreserving_edgeLabels line 43
  6. theorem OAI.Problem367.EdgeIIDLaw.measurePreserving_environment_edgeLabels line 53
  7. theorem OAI.Problem367.EdgeIIDLaw.coded_all_open line 75
  8. theorem OAI.Problem367.EdgeIIDLaw.coded_joint_cylinder line 81
  9. abbrev OAI.Problem367.EdgeIIDLaw.VertexInput line 94
  10. abbrev OAI.Problem367.EdgeIIDLaw.vertexInputLaw line 96
  11. abbrev OAI.Problem367.EdgeIIDLaw.vertexInputMeasure line 99
  12. def OAI.Problem367.EdgeIIDLaw.splitVertexInputs line 102
  13. theorem OAI.Problem367.EdgeIIDLaw.measurePreserving_splitVertexInputs line 106
  14. def OAI.Problem367.EdgeIIDLaw.vertexEdgeLabels line 126
  15. theorem OAI.Problem367.EdgeIIDLaw.measurePreserving_vertex_priority_edges line 130
  16. theorem OAI.Problem367.EdgeIIDLaw.measurePreserving_vertexEdgeLabels line 136
  17. def OAI.Problem367.EdgeIIDLaw.vertexEdgeLabel line 140
  18. theorem OAI.Problem367.EdgeIIDLaw.vertexEdgeLabel_relabel line 144
  19. theorem OAI.Problem367.EdgeIIDLaw.ae_vertexEdgeLabel_symmetric line 149
  20. theorem OAI.Problem367.EdgeIIDLaw.vertex_coded_all_open line 163