OAI/Probability/FirstPassage/UnitSphereC1.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarFPP.actual_profile_contDiff line 11
2. lemma OAI.PlanarFPP.plane_direction_representation line 28
3. lemma OAI.PlanarFPP.actual_contDiffAt_horizontal line 34
4. theorem OAI.PlanarFPP.actual_contDiffAt_away line 60
5. theorem OAI.PlanarFPP.actual_C1_unit_sphere line 76