OAI/Analysis/HardSphere/Geometry/AllowedProjection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.killedAverage_zero_of_not_allowed line 20
2. def OAI.HardSphere.allowedProjection line 32
3. lemma OAI.HardSphere.allowedProjection_ae line 36
4. lemma OAI.HardSphere.killedTransition_zero line 44
5. lemma OAI.HardSphere.allowedProjection_killedTransition line 59
6. lemma OAI.HardSphere.killedTransition_allowedProjection line 75
7. lemma OAI.HardSphere.killedTransition_support line 83
8. lemma OAI.HardSphere.killedTransition_add_nonneg line 93
9. lemma OAI.HardSphere.exists_bounded_lift_of_tendsto line 105