OAI/Analysis/HardSphere/Geometry/AuxiliaryChecks.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Comparison.auxiliaryChecks line 22
2. lemma OAI.HardSphere.Comparison.auxiliary_checkWeight line 36
3. def OAI.HardSphere.Comparison.auxiliaryDensity line 40
4. lemma OAI.HardSphere.Comparison.auxiliaryDensity_delete_le line 43
5. lemma OAI.HardSphere.Comparison.auxiliaryDensity_depends line 50
6. lemma OAI.HardSphere.Comparison.measurable_auxiliaryDensity line 66
7. lemma OAI.HardSphere.Comparison.auxiliaryDensity_integral line 82
8. def OAI.HardSphere.Comparison.densityProduct line 115
9. lemma OAI.HardSphere.Comparison.measurable_densityProduct line 119
10. lemma OAI.HardSphere.Comparison.densityProduct_depends line 124
11. lemma OAI.HardSphere.Comparison.densityProduct_union line 130
12. lemma OAI.HardSphere.Comparison.lmarginal_overlap_products line 142
13. lemma OAI.HardSphere.Comparison.dependsOn_mul_union line 181
14. lemma OAI.HardSphere.Comparison.auxiliaryDensity_overlap_bound line 201
15. def OAI.HardSphere.Comparison.UniformInsertionOn line 257
16. lemma OAI.HardSphere.Comparison.insertion_integral_lower_on line 263
17. def OAI.HardSphere.Comparison.partialNormalizer line 280
18. lemma OAI.HardSphere.Comparison.partialNormalizer_insert_lower line 283
19. lemma OAI.HardSphere.Comparison.partialNormalizer_union_lower line 300
20. lemma OAI.HardSphere.Comparison.partialNormalizer_pos line 326
21. lemma OAI.HardSphere.Comparison.partialNormalizer_far_eq line 337
22. lemma OAI.HardSphere.Comparison.partialNormalizer_le_far line 358
23. def OAI.HardSphere.Comparison.conditionalDensity line 380
24. lemma OAI.HardSphere.Comparison.conditionalDensity_le_auxiliaryDensity line 385
25. lemma OAI.HardSphere.Comparison.measurable_conditionalDensity line 391
26. lemma OAI.HardSphere.Comparison.conditionalDensity_integral line 407