OAI/Analysis/HardSphere/Allocation/Allocation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.Sampling.Allocation line 17
  2. instance OAI.HardSphere.Sampling.allocationMeasurable line 18
  3. instance OAI.HardSphere.Sampling.allocationSingletons line 19
  4. instance OAI.HardSphere.Sampling.allocationFintype line 20
  5. def OAI.HardSphere.Sampling.allocationPMF line 22
  6. lemma OAI.HardSphere.Sampling.allocationPMF_large line 30
  7. lemma OAI.HardSphere.Sampling.allocationPMF_small line 36
  8. lemma OAI.HardSphere.Sampling.allocationPMF_support line 40
  9. def OAI.HardSphere.Sampling.allocationKernel line 55
  10. instance OAI.HardSphere.Sampling.allocationKernel_markov line 57
  11. lemma OAI.HardSphere.Sampling.allocated_group_uniform line 61
  12. lemma OAI.HardSphere.Sampling.allocation_half_bad line 75
  13. def OAI.HardSphere.Groups.Confined line 140
  14. lemma OAI.HardSphere.Groups.confined_closed line 143
  15. def OAI.HardSphere.Groups.EndpointEligible line 150
  16. lemma OAI.HardSphere.Groups.endpointEligible_measurable line 156
  17. def OAI.HardSphere.Groups.Eligible line 176
  18. lemma OAI.HardSphere.Groups.eligible_measurable line 181
  19. def OAI.HardSphere.Groups.eligibleList line 188
  20. lemma OAI.HardSphere.Groups.eligibleList_disjoint line 192
  21. lemma OAI.HardSphere.Groups.eligibleList_measurable line 201