OAI/Analysis/HardSphere/Allocation/PhysicalAssembly.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Comparison.finite_allocation_joint line 15
2. lemma OAI.HardSphere.Comparison.recorded_density_sum line 41
3. lemma OAI.HardSphere.Comparison.allocated_flag_joint line 63
4. lemma OAI.HardSphere.Comparison.map_retained_compProd line 100
5. lemma OAI.HardSphere.Comparison.allocated_exposure_joint line 121
6. lemma OAI.HardSphere.Comparison.allocationBase_ae_support line 159
7. lemma OAI.HardSphere.Comparison.exposed_endpoint_ae line 174
8. lemma OAI.HardSphere.Groups.recorded_allocation_is_physical line 189
9. lemma OAI.HardSphere.Groups.genuine_ground_allocated_joint line 214
10. lemma OAI.HardSphere.Groups.allocated_selected_flags line 268
11. lemma OAI.HardSphere.Groups.true_flag_endpoint line 286
12. lemma OAI.HardSphere.Groups.exposed_selected_endpoints line 297
13. def OAI.HardSphere.Groups.exposedAnchorLift line 318
14. lemma OAI.HardSphere.Groups.exposedAnchorLift_project line 322
15. lemma OAI.HardSphere.Groups.exposedAnchorLift_near line 327
16. def OAI.HardSphere.Groups.ExposedPhysicalIdentity line 338
17. lemma OAI.HardSphere.Groups.canonical_physical_reference line 353
18. theorem OAI.HardSphere.Groups.actual_allocated_physical_reference line 369