OAI/Probability/ClassicalON/LatticeGeometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.latticeAxis line 9
  2. def OAI.ClassicalON.latticeTorus line 11
  3. theorem OAI.ClassicalON.latticeTorus_add line 13
  4. def OAI.ClassicalON.scaledSite line 17
  5. theorem OAI.ClassicalON.scaledSite_add_axis line 20
  6. def OAI.ClassicalON.LatticeGraph.edgeDirection line 26
  7. theorem OAI.ClassicalON.LatticeGraph.edge_step line 29
  8. abbrev OAI.ClassicalON.LatticeGraph.DirectionalEdges line 38
  9. theorem OAI.ClassicalON.LatticeGraph.directional_origin_injective line 40
  10. def OAI.ClassicalON.LatticeGraph.WithinDyadicBox line 55
  11. theorem OAI.ClassicalON.LatticeGraph.torus_site_injective line 58
  12. theorem OAI.ClassicalON.LatticeGraph.directional_torus_injective line 76
  13. theorem OAI.ClassicalON.LatticeGraph.edge_card_bound line 80
  14. theorem OAI.ClassicalON.LatticeGraph.scaled_edge_distance line 99