OAI/Analysis/HardSphere/PathBounds/GridTailTransfer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Groups.joint_event_image line 17
2. lemma OAI.HardSphere.Groups.grid_visitors_eq line 24
3. lemma OAI.HardSphere.Groups.grid_longVisitors_eq line 33
4. lemma OAI.HardSphere.Groups.grid_nonregular_iff line 43
5. lemma OAI.HardSphere.Groups.ofReal_power_tail line 56
6. lemma OAI.HardSphere.Groups.exp_power_tail line 61
7. lemma OAI.HardSphere.Groups.grid_close_tail line 66