OAI/Analysis/HardSphere/Bridges/GaussianDensity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.GaussianPacking.density line 11
2. lemma OAI.HardSphere.GaussianPacking.density_nonneg line 12
3. lemma OAI.HardSphere.GaussianPacking.density_continuous line 13
4. lemma OAI.HardSphere.GaussianPacking.density_integrable line 14
5. lemma OAI.HardSphere.GaussianPacking.density_integral line 16
6. lemma OAI.HardSphere.GaussianPacking.sum_density_le line 22
7. def OAI.HardSphere.GaussianPacking.packingConstant line 44
8. lemma OAI.HardSphere.GaussianPacking.packingConstant_pos line 45
9. theorem OAI.HardSphere.GaussianPacking.density_packing line 47
10. def OAI.HardSphere.GaussianPacking.gaussianDensity line 84
11. lemma OAI.HardSphere.GaussianPacking.gaussianDensity_nonneg line 85
12. lemma OAI.HardSphere.GaussianPacking.gaussianDensity_integrable line 87
13. lemma OAI.HardSphere.GaussianPacking.gaussianDensity_measurable line 89
14. theorem OAI.HardSphere.GaussianPacking.gaussian_pi_density line 93
15. lemma OAI.HardSphere.GaussianPacking.gaussianDensity_eq line 107
16. lemma OAI.HardSphere.GaussianPacking.gaussian_pi_eq line 125