OAI/Analysis/HardSphere/Geometry/BufferedAllowed.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.killedLaplace_innerRadius_tendsto line 20
2. def OAI.HardSphere.bufferedAllowed line 40
3. lemma OAI.HardSphere.bufferedAllowed_closed line 43
4. lemma OAI.HardSphere.allowed_subset_buffered line 58
5. lemma OAI.HardSphere.bufferedAllowed_subset line 61
6. lemma OAI.HardSphere.killedLaplace_buffered_graph line 64
7. lemma OAI.HardSphere.killedLaplace_graph line 84