OAI/Probability/FirstPassage/ConnectorGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFPP.connectorWindow line 11
  2. def OAI.PlanarFPP.connectorRegion line 14
  3. theorem OAI.PlanarFPP.connectorRegion_finite line 18
  4. def OAI.PlanarFPP.connectorVertices line 25
  5. theorem OAI.PlanarFPP.mem_connectorVertices line 28
  6. theorem OAI.PlanarFPP.connector_transverse_displacement line 32
  7. theorem OAI.PlanarFPP.connector_window_bounds line 54
  8. theorem OAI.PlanarFPP.transverse_plane_lipschitz line 72
  9. theorem OAI.PlanarFPP.plane_norm_le_shear line 82
  10. theorem OAI.PlanarFPP.connector_union_diameter line 92
  11. theorem OAI.PlanarFPP.connector_tube_containment line 114