OAI/Probability/GammaPassage/ConnectorGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GammaFPP.CrossingBridge.connectorWindow line 10
  2. def OAI.GammaFPP.CrossingBridge.connectorRegion line 13
  3. theorem OAI.GammaFPP.CrossingBridge.connectorRegion_finite line 17
  4. def OAI.GammaFPP.CrossingBridge.connectorVertices line 24
  5. theorem OAI.GammaFPP.CrossingBridge.mem_connectorVertices line 27
  6. theorem OAI.GammaFPP.CrossingBridge.connector_transverse_displacement line 31
  7. theorem OAI.GammaFPP.CrossingBridge.connector_window_bounds line 53
  8. theorem OAI.GammaFPP.CrossingBridge.transverse_plane_lipschitz line 71
  9. theorem OAI.GammaFPP.CrossingBridge.plane_norm_le_shear line 81
  10. theorem OAI.GammaFPP.CrossingBridge.connector_union_diameter line 91
  11. theorem OAI.GammaFPP.CrossingBridge.connector_tube_containment line 113