Extrema of the N-dim Rosenbrock function

Stream: general

[Henrik Böving]

I recently wrote a proof that this definition of the n dimensional Rosenbrock function (for even N):
$f(x_1, \dots, x_n) = \sum_{i=1}^{n/2} ((x_{2-i} -1)^2 + 100 \cdot (x_{2i-1}^2 - x_{2i})^2)$
has exactly one extremum (namely at (1,1,1...)) for my numerics class. My proof was basically computing the gradient and showing that it cannot be equal to 0 unless every component of the input vector = 1.

Now I'd be curious if this is nicely ish to formalize in Lean 3? I'd guess that the n/2 will make some problems and I should instead work with some m and some n = 2 * m for the definition. But generally speaking is it possible for someone with relatively little experience in mathlib (and especially in the calculus parts of mathlib) to formalize this? Which modules would I specifically want to take a look into?

[Reid Barton]

Probably an unhelpful comment but I think it would be easier to skip the calculus--it's a sum of squares and all the quantities being squared are zero at that point (1,1,1,...) and nowhere else.

[Reid Barton]

Oh extremum means local extremum?

[Henrik Böving]

Oh yes sorry, local extremum.