OAI/Analysis/HardSphere/Conditioning/WeightedUnitPairCount.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.unitOccupation_le line 23
  2. lemma OAI.HardSphere.unitPairCount_le line 28
  3. lemma OAI.HardSphere.unitPairCount_integrable line 36
  4. lemma OAI.HardSphere.localizedNearLabels_integrable line 42
  5. def OAI.HardSphere.weightedUnitPairCount line 47
  6. lemma OAI.HardSphere.weightedUnitPairCount_nonneg line 51
  7. lemma OAI.HardSphere.weightedUnitPairCount_integral line 55
  8. lemma OAI.HardSphere.weightedUnitPairCount_integrable line 65
  9. lemma OAI.HardSphere.spatial_cell_average_real line 71
  10. lemma OAI.HardSphere.spatial_near_average_real line 96
  11. theorem OAI.HardSphere.spatial_before_square line 110