OAI/Probability/FirstPassage/PlaneGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.direction line 9
  2. def OAI.PlanarFPP.transverseUnit line 10
  3. def OAI.PlanarFPP.xCoord line 11
  4. def OAI.PlanarFPP.rCoord line 12
  5. theorem OAI.PlanarFPP.xCoord_apply line 15
  6. theorem OAI.PlanarFPP.rCoord_apply line 16
  7. theorem OAI.PlanarFPP.xCoord_direction line 17
  8. theorem OAI.PlanarFPP.rCoord_direction line 18
  9. theorem OAI.PlanarFPP.plane_reconstruction line 21
  10. theorem OAI.PlanarFPP.norm_positive_homogeneous line 27
  11. theorem OAI.PlanarFPP.planar_extreme_supports line 32
  12. theorem OAI.PlanarFPP.planar_differentiability_of_no_corner line 46