OAI/Probability/FirstPassage/TimeConstantObligation.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PlanarFPP.TimeConstantExistenceTargetline 9 - def
OAI.PlanarFPP.FullMainDifferentiabilityTargetline 14 - theorem
OAI.PlanarFPP.isTimeConstant_uniqueline 20