OAI/Analysis/HardSphere/Geometry/FilledRegion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.BathSlice.coordinate_dist_lift_le line 16
  2. lemma OAI.HardSphere.BathSlice.volume_microCube_le line 21
  3. def OAI.HardSphere.BathSlice.filledRegion line 46
  4. lemma OAI.HardSphere.BathSlice.volume_finite_microCubes_le line 49
  5. lemma OAI.HardSphere.BathSlice.volume_filledRegion_le_columns line 59
  6. theorem OAI.HardSphere.BathSlice.volume_small_filledRegion line 78
  7. def OAI.HardSphere.BathSlice.witnessBox line 95
  8. lemma OAI.HardSphere.BathSlice.card_witnessBox line 99
  9. lemma OAI.HardSphere.BathSlice.interval_ball_witness line 109
  10. lemma OAI.HardSphere.BathSlice.ball_microCube_witness line 123
  11. theorem OAI.HardSphere.BathSlice.ncard_ball_bad_sites_le line 161