OAI/Probability/FreeIsing/Estimates/SeparatedLocalSupports.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.LocalSupportGeometry.prefixVertex line 10
2. theorem OAI.Problem367.LocalSupportGeometry.prefixVertex_length line 13
3. theorem OAI.Problem367.LocalSupportGeometry.prefixVertex_prefix line 17
4. theorem OAI.Problem367.LocalSupportGeometry.prefix_image_of_root_prefix line 20
5. theorem OAI.Problem367.LocalSupportGeometry.image_ball_prefix line 46
6. theorem OAI.Problem367.LocalSupportGeometry.separated_ball_endpoints line 55