OAI/Analysis/HardSphere/Geometry/LocalizedNearLabels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.spatialSiteDistance_triangle line 23
  2. lemma OAI.HardSphere.spatialOutside_zero line 29
  3. lemma OAI.HardSphere.productPartition_norm_unity line 36
  4. lemma OAI.HardSphere.spatialPartition_forces_inside line 43
  5. def OAI.HardSphere.localizedNearLabels line 54
  6. lemma OAI.HardSphere.localizedNearLabels_card_le_selected line 60
  7. lemma OAI.HardSphere.spatialPartition_near_weight line 81
  8. lemma OAI.HardSphere.measurable_close_predicate line 105
  9. lemma OAI.HardSphere.measurable_near_predicate line 111
  10. lemma OAI.HardSphere.nearLabels_card_measurable line 117
  11. lemma OAI.HardSphere.measurable_localized_near_predicate line 126
  12. lemma OAI.HardSphere.localizedNearLabels_card_measurable line 134
  13. lemma OAI.HardSphere.spatialPartition_near_integral line 144
  14. theorem OAI.HardSphere.spatial_near_average line 176