OAI/Analysis/HardSphere/Bridges/SupplyIntegral.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Bridge.SuccessExcept line 17
2. lemma OAI.HardSphere.Bridge.successExcept_measurable line 21
3. lemma OAI.HardSphere.Bridge.trial_no_collision_far line 29
4. lemma OAI.HardSphere.Bridge.failure_except_le line 39
5. lemma OAI.HardSphere.Bridge.failure_integral_sum line 66
6. lemma OAI.HardSphere.Bridge.physical_failure_sum line 116