OAI/Analysis/HardSphere/Allocation/PhysicalFamilyLikelihood.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Groups.physicalRouteView line 17
  2. instance OAI.HardSphere.Groups.physicalRouteView_finite line 22
  3. def OAI.HardSphere.Groups.physicalFamilyReference line 28
  4. instance OAI.HardSphere.Groups.physicalFamilyReference_finite line 33
  5. def OAI.HardSphere.Groups.physicalRouteLikelihood line 38
  6. lemma OAI.HardSphere.Groups.physicalRouteLikelihood_measurable line 43
  7. lemma OAI.HardSphere.Groups.physicalRouteLikelihood_measure line 48
  8. lemma OAI.HardSphere.Groups.uniformFinset_subtype line 79
  9. lemma OAI.HardSphere.Groups.paddedLabels_card line 100
  10. lemma OAI.HardSphere.Groups.label_pair_transport line 104
  11. def OAI.HardSphere.Groups.fieldLabelImage line 137
  12. lemma OAI.HardSphere.Groups.padded_label_overlap line 140
  13. lemma OAI.HardSphere.Groups.fieldLabelImage_eq line 176
  14. lemma OAI.HardSphere.Groups.fieldRoute_overlap line 182