OAI/Analysis/HardSphere/Geometry/LargeParentMarked.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.BathSlice.LargeParentMarked line 15
  2. theorem OAI.HardSphere.BathSlice.finite_components_of_no_large line 22
  3. theorem OAI.HardSphere.BathSlice.large_finite_parent_lift line 40
  4. def OAI.HardSphere.BathSlice.rootBox line 68
  5. lemma OAI.HardSphere.BathSlice.volume_rootBox_le line 71
  6. lemma OAI.HardSphere.BathSlice.scaled_parent_bounds line 81
  7. lemma OAI.HardSphere.BathSlice.filledRegion_subset_rootBox line 100
  8. lemma OAI.HardSphere.BathSlice.coarseCenter_eq_of_projection line 123
  9. lemma OAI.HardSphere.BathSlice.rootBox_eq_of_projection line 139
  10. def OAI.HardSphere.BathSlice.siteRep line 148
  11. lemma OAI.HardSphere.BathSlice.siteRep_projection line 150
  12. def OAI.HardSphere.BathSlice.siteCenter line 156
  13. def OAI.HardSphere.BathSlice.closeSet line 159
  14. theorem OAI.HardSphere.BathSlice.actual_large_parent_marked line 164
  15. def OAI.HardSphere.BathSlice.largeBoxUnion line 179
  16. theorem OAI.HardSphere.BathSlice.omitted_subset_small_and_boxes line 183