OAI/Probability/LatticeSurface/Geometry/BlockVolume.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TriangularLipschitz.mem_interior line 15
  2. lemma OAI.TriangularLipschitz.interior_subset_box line 20
  3. lemma OAI.TriangularLipschitz.origin_not_interior line 25
  4. lemma OAI.TriangularLipschitz.filledHeight_free line 28
  5. lemma OAI.TriangularLipschitz.filledHeight_fixed line 32
  6. lemma OAI.TriangularLipschitz.continuous_filledHeight line 36
  7. lemma OAI.TriangularLipschitz.isClosed_fillingPolytope line 43
  8. lemma OAI.TriangularLipschitz.measurableSet_fillingPolytope line 51
  9. def OAI.TriangularLipschitz.filledHeightAffine line 54
  10. lemma OAI.TriangularLipschitz.filledHeightAffine_apply line 59
  11. lemma OAI.TriangularLipschitz.convex_fillingPolytope line 64
  12. lemma OAI.TriangularLipschitz.latticeDist_origin_le line 78
  13. lemma OAI.TriangularLipschitz.fillingPolytope_subset_closedBall line 91
  14. lemma OAI.TriangularLipschitz.fillingVolume_lt_top line 101
  15. lemma OAI.TriangularLipschitz.isCompact_fillingPolytope line 104
  16. lemma OAI.TriangularLipschitz.filledHeight_center line 109
  17. lemma OAI.TriangularLipschitz.filledHeight_perturbation line 114
  18. lemma OAI.TriangularLipschitz.ball_subset_fillingPolytope line 122
  19. lemma OAI.TriangularLipschitz.fillingVolume_pos_of_strict line 142