OAI/Probability/FirstPassage/ExtremeSlopes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.leftSlope line 9
2. def OAI.PlanarFPP.rightSlope line 10
3. theorem OAI.PlanarFPP.extreme_slopes_ordered line 12
4. theorem OAI.PlanarFPP.subgradient_of_between_slopes line 16
5. theorem OAI.PlanarFPP.extreme_subgradients line 33
6. theorem OAI.PlanarFPP.extreme_slopes_contact line 40
7. theorem OAI.PlanarFPP.convex_transverse_profile line 46
8. theorem OAI.PlanarFPP.extreme_supports line 60