OAI/Analysis/HardSphere/Bridges/AffineVolume.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.GaussianPacking.affine line 11
2. lemma OAI.HardSphere.GaussianPacking.affine_measurable line 12
3. lemma OAI.HardSphere.GaussianPacking.affine_volume line 13
4. lemma OAI.HardSphere.GaussianPacking.affine_restrict_le line 25
5. lemma OAI.HardSphere.GaussianPacking.affine_kernel_le line 30
6. lemma OAI.HardSphere.Bridge.leg_segment_increment line 55
7. def OAI.HardSphere.Bridge.uniformSegmentHit line 62
8. lemma OAI.HardSphere.Bridge.uniform_segment_necessary line 65
9. lemma OAI.HardSphere.Bridge.uniform_position_le line 95
10. lemma OAI.HardSphere.Bridge.uniform_segment_bound line 109