OAI/Probability/LatticeSurface/Geometry/BlockFacetGeometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularLipschitz.shell_eq_box_not_interior line 30
2. lemma OAI.TriangularLipschitz.latticeDist_box_le line 33
3. lemma OAI.TriangularLipschitz.endpoint_shell_difference line 46
4. lemma OAI.TriangularLipschitz.filledHeight_constant_shift line 63
5. lemma OAI.TriangularLipschitz.filledHeight_base_difference line 67
6. lemma OAI.TriangularLipschitz.filledHeight_change_bound line 76
7. lemma OAI.TriangularLipschitz.filledHeight_edge_change_bound line 84
8. lemma OAI.TriangularLipschitz.shifted_exposure line 95
9. lemma OAI.TriangularLipschitz.filling_of_small_perturbation_on_facet line 115
10. lemma OAI.TriangularLipschitz.ball_subset_polytope_of_slack line 138
11. lemma OAI.TriangularLipschitz.fillingVolume_pos_of_slack line 152
12. lemma OAI.TriangularLipschitz.filledHeight_mix line 160
13. lemma OAI.TriangularLipschitz.fillingPolytope_mix line 166
14. lemma OAI.TriangularLipschitz.fillingVolume_interpolated_pos line 183