OAI/Probability/LatticeSurface/Geometry/ContactVolume.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.StrictFilling.FreeCoord line 27
2. def OAI.StrictFilling.restore line 29
3. def OAI.StrictFilling.conditionalBody line 33
4. def OAI.StrictFilling.contactRegion line 38
5. def OAI.StrictFilling.restoreAffine line 43
6. lemma OAI.StrictFilling.restoreAffine_apply line 48
7. lemma OAI.StrictFilling.restore_fixed line 54
8. lemma OAI.StrictFilling.restore_free line 58
9. lemma OAI.StrictFilling.conditionalBody_convex line 62
10. theorem OAI.StrictFilling.graph_conditional_contact_volume line 83