The work by Thomas Hales (see enter link description here) before the formal proof solves a number of global optimization problems that need to be solved exactly.
The strategy relies on following strategy:
- Use of interval arithmetic in order to be sure of where the values are located.
- Use of linearization, bounds on derivative and linear programming in order to get lower bounds on a specific domain.
- Use of domain decomposition (branch and bounds) in order to decompose domains where the conclusion can be reached.
- Use of Taylor expansion in order to conclude near the minimum of the function.
This kind of method can be applied to general global optimization problems, not just the one of Kepler problem. What has been done in this vein after Hales. Surely many mathematical problems can be solved with such methodology. What is the state of the art in this respect? I am not interested in algebraic geometry approaches. I am also not interested in stochastic or heuristic methods that do not provide rigorous solutions.
The problem I want to consider is in a polyhedral domain of dimension 9. The function to be minimized is a fraction of two polynomials. I would expect that it can be solved reasonably easily.
I would expect that a general purpose software had been written on this but I do not know any so far.