OAI/Probability/FirstPassage/SupportContactEstimate.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PlanarFPP.derivative_remainder_radiusline 9 - def
OAI.PlanarFPP.extremeSlopeline 22 - def
OAI.PlanarFPP.contactSideline 26 - theorem
OAI.PlanarFPP.norm_extreme_support_contactline 28 - theorem
OAI.PlanarFPP.connector_support_gapline 54