OAI/Probability/LatticeSurface/Geometry/BlockEdgeGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularLipschitz.edgeOffset line 58
  2. lemma OAI.TriangularLipschitz.exists_filling_edge_coordinates line 61
  3. lemma OAI.TriangularLipschitz.filling_projection_width line 81
  4. lemma OAI.TriangularLipschitz.filling_facet_ball line 95
  5. lemma OAI.TriangularLipschitz.linearCoordinates_measurableEmbedding line 138
  6. lemma OAI.TriangularLipschitz.filling_volume_image line 142
  7. lemma OAI.TriangularLipschitz.isCompact_filling_image line 148
  8. lemma OAI.TriangularLipschitz.convex_filling_image line 152
  9. lemma OAI.TriangularLipschitz.filling_image_volume_bound line 156
  10. def OAI.TriangularLipschitz.meanHeight line 167
  11. lemma OAI.TriangularLipschitz.integrableOn_filledHeight line 170
  12. lemma OAI.TriangularLipschitz.meanHeight_fixed line 174
  13. lemma OAI.TriangularLipschitz.coordinate_meanHeight line 182