OAI/Probability/SKBarriers/Calculus/ParameterSpace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.ParameterSpace line 19
2. instance OAI.SK.Analytic.parameterNormedGroup line 23
3. instance OAI.SK.Analytic.parameterNormedSpace line 27
4. instance OAI.SK.Analytic.parameterFiniteDimensional line 31
5. def OAI.SK.Analytic.coordinateSquare line 35
6. theorem OAI.SK.Analytic.coordinateSquare_zero line 39
7. theorem OAI.SK.Analytic.coordinateSquare_nonneg line 47
8. def OAI.SK.Analytic.cubePotential line 53
9. theorem OAI.SK.Analytic.cubePotential_hessian_lower line 57