Zulip Chat Archive

Stream: general

Topic: Extrema of the N-dim Rosenbrock function

Henrik Böving (Jan 26 2022 at 15:47):

I recently wrote a proof that this definition of the n dimensional Rosenbrock function (for even N):
f(x1,,xn)=i=1n/2((x2i1)2+100(x2i12x2i)2)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 (Jan 26 2022 at 16:05):

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 (Jan 26 2022 at 16:06):

Oh extremum means local extremum?

Henrik Böving (Jan 26 2022 at 16:13):

Oh yes sorry, local extremum.

Last updated: Aug 03 2023 at 10:10 UTC