OAI/Analysis/HardSphere/Geometry/GridAllocation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.Groups.GridAllocation line 17
  2. def OAI.HardSphere.Groups.gridAllocationKernel line 19
  3. lemma OAI.HardSphere.Groups.gridAllocationKernel_apply line 23
  4. instance OAI.HardSphere.Groups.gridAllocationKernel_markov line 29
  5. def OAI.HardSphere.Groups.groupPosition line 36
  6. lemma OAI.HardSphere.Groups.groupPosition_disjoint line 46
  7. def OAI.HardSphere.Groups.groupAt line 64
  8. def OAI.HardSphere.Groups.groupUnion line 69
  9. lemma OAI.HardSphere.Groups.groupAt_mem_list line 72
  10. lemma OAI.HardSphere.Groups.groups_disjoint line 84
  11. lemma OAI.HardSphere.Groups.allocation_support_ae line 117
  12. lemma OAI.HardSphere.Groups.gridAllocation_support_ae line 123
  13. lemma OAI.HardSphere.Groups.groups_disjoint_ae line 132
  14. lemma OAI.HardSphere.Groups.pi_failure_sets line 138
  15. lemma OAI.HardSphere.Groups.grid_group_law line 152