OAI/Probability/SKBarriers/Calculus/MarginalPotential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.hasDerivAt_score_comp line 19
2. def OAI.SK.Analytic.marginalPotential line 30
3. theorem OAI.SK.Analytic.contDiff_marginalPotential line 33
4. theorem OAI.SK.Analytic.marginal_hessian_lower line 42