theory Unconstrained_Optimization imports Auxilary_Facts Minimizers_Definition First_Order_Conditions Second_Derivative_Test Cont_Nonisolated_Strict_Local_Minimizer_Exists begin end