OAI/Probability/CriticalPercolation/Criticality/SquareBoundary.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CriticalPercolation.Boundary.Grid line 14
  2. abbrev OAI.CriticalPercolation.Boundary.Dir line 15
  3. abbrev OAI.CriticalPercolation.Boundary.Edge line 16
  4. def OAI.CriticalPercolation.Boundary.step line 18
  5. def OAI.CriticalPercolation.Boundary.leftOffset line 19
  6. def OAI.CriticalPercolation.Boundary.rightOffset line 20
  7. def OAI.CriticalPercolation.Boundary.tail line 21
  8. def OAI.CriticalPercolation.Boundary.head line 22
  9. def OAI.CriticalPercolation.Boundary.leftSite line 23
  10. def OAI.CriticalPercolation.Boundary.rightSite line 24
  11. def OAI.CriticalPercolation.Boundary.squareBoundary line 26
  12. lemma OAI.CriticalPercolation.Boundary.squareBoundary_finite line 29
  13. def OAI.CriticalPercolation.Boundary.outgoingEquiv line 40
  14. def OAI.CriticalPercolation.Boundary.incomingEquiv line 55
  15. lemma OAI.CriticalPercolation.Boundary.squareBoundary_balanced line 71
  16. theorem OAI.CriticalPercolation.Boundary.squareBoundary_closed_trail line 84
  17. lemma OAI.CriticalPercolation.Boundary.west_root_edge_mem line 101