OAI/Probability/FreeIsing/Estimates/CylinderAutomorphism.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ConnectedFinset.image line 13
  2. theorem OAI.Problem367.CylinderAut.adj_symm line 28
  3. theorem OAI.Problem367.CylinderAut.length_ne_of_adj line 31
  4. def OAI.Problem367.CylinderAut.orient line 39
  5. theorem OAI.Problem367.CylinderAut.orient_swap line 42
  6. theorem OAI.Problem367.CylinderAut.mem_inducedEdges line 49
  7. theorem OAI.Problem367.CylinderAut.orient_mem line 56
  8. theorem OAI.Problem367.CylinderAut.orient_eq_of_mem line 66
  9. def OAI.Problem367.CylinderAut.push line 71
  10. def OAI.Problem367.CylinderAut.pull line 75
  11. theorem OAI.Problem367.CylinderAut.push_mem line 79
  12. theorem OAI.Problem367.CylinderAut.pull_push line 87
  13. theorem OAI.Problem367.CylinderAut.pull_mem line 95
  14. theorem OAI.Problem367.CylinderAut.push_pull line 111
  15. theorem OAI.Problem367.CylinderAut.prod_inducedEdges_image line 119
  16. theorem OAI.Problem367.freeCylinderWeight_image_relabel line 144
  17. def OAI.Problem367.cylinderInverseAut line 156
  18. theorem OAI.Problem367.measurable_spin_cylinder line 162
  19. theorem OAI.Problem367.HasFreeIsingLaw.map_relabel line 172