OAI/Geometry/CylinderCovering/Singular/EdgeOneGeometry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingularEdgeOne.fieldP_eq_ruled line 13
  2. lemma OAI.SingularEdgeOne.fieldQ_eq_ruled line 20
  3. lemma OAI.SingularEdgeOne.ceiling_eq_ruled line 26
  4. lemma OAI.SingularEdgeOne.coefficient_eq_ruled line 30
  5. lemma OAI.SingularEdgeOne.edgeDomain0_isCompact line 32
  6. lemma OAI.SingularEdgeOne.edgeEnergy_eq_ruled line 44
  7. lemma OAI.SingularEdgeOne.edgeEnergy_nonneg line 50
  8. lemma OAI.SingularEdgeOne.edgeEnergy_measurable line 54
  9. lemma OAI.SingularEdgeOne.edgeEnergy_on_domain_eq line 59
  10. lemma OAI.SingularEdgeOne.edgeEnergy_integrable line 67
  11. lemma OAI.SingularEdgeOne.edgeG_integral line 81
  12. lemma OAI.SingularEdgeOne.height_factor line 108
  13. lemma OAI.SingularEdgeOne.physicalSimilarity_vec3 line 113
  14. lemma OAI.SingularEdgeOne.physicalSimilarity_tetrahedron line 116
  15. lemma OAI.SingularEdgeOne.edgeU_labelMap line 142
  16. lemma OAI.SingularEdgeOne.edgeV_labelMap line 147
  17. lemma OAI.SingularEdgeOne.physicalSimilarity_lower line 153
  18. lemma OAI.SingularEdgeOne.physicalSimilarity_upper line 195
  19. lemma OAI.SingularEdgeOne.upperSegments_canonical line 235