OAI/Probability/ClassicalON/LatticeRadius.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.siteRadius line 10
  2. theorem OAI.ClassicalON.siteRadius_self line 12
  3. theorem OAI.ClassicalON.siteRadius_nonneg line 14
  4. theorem OAI.ClassicalON.siteRadius_symm line 16
  5. theorem OAI.ClassicalON.siteRadius_le_iff line 19
  6. theorem OAI.ClassicalON.siteRadius_triangle line 22
  7. theorem OAI.ClassicalON.siteRadius_neighbor line 37
  8. theorem OAI.ClassicalON.siteRadius_neighbor_step line 40
  9. def OAI.ClassicalON.annulusSites line 51
  10. def OAI.ClassicalON.annulusBoundary line 53
  11. def OAI.ClassicalON.annulusInterior line 55
  12. theorem OAI.ClassicalON.annulusSites_not_boundary line 57
  13. theorem OAI.ClassicalON.neighbor_in_annulus line 62
  14. theorem OAI.ClassicalON.annuli_disjoint line 69
  15. def OAI.ClassicalON.LatticeGraph.annulusGraph line 81
  16. def OAI.ClassicalON.LatticeGraph.annulusInner line 83
  17. def OAI.ClassicalON.LatticeGraph.annulusOuter line 86
  18. def OAI.ClassicalON.LatticeGraph.annulusPins line 89
  19. def OAI.ClassicalON.LatticeGraph.annulusCoupling line 92