Zulip Chat Archive

Stream: Is there code for X?

Topic: Local vs global minimum


view this post on Zulip Frédéric Dupuis (Jul 17 2020 at 18:29):

Hi,

Does anyone know whether there is a lemmas somewhere that says that a local minimum of a convex function is a global minimum (or anything along those lines)?

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 15:38):

AFAIK, no. Are you going to formalize and PR it?

view this post on Zulip Frédéric Dupuis (Jul 18 2020 at 17:46):

Yes, I think I'll give it a shot!

view this post on Zulip Frédéric Dupuis (Jul 19 2020 at 19:34):

I'm slowly getting there, but along the way I stumbled on some missing lemmas that should probably go in topology.local_extr; I guess I should probably PR those separately first...?

view this post on Zulip Frédéric Dupuis (Jul 19 2020 at 19:35):

Basically just stuff like:

lemma is_local_min_on.comp_continuous_on [topological_space δ] {s : set δ} {g : δ  α} {b : δ}
  (hf : is_local_min_on f (g '' s) (g b)) (hg : continuous_on g s) (hb : b  s) :
  is_local_min_on (f  g) s b :=
hf.comp_tendsto (continuous_within_at.tendsto_nhds_within_image (hg b hb))

view this post on Zulip Sebastien Gouezel (Jul 19 2020 at 19:46):

Yes, this kind of lemma definitely makes sense for mathlib. One remark though about this one: images of sets are not really well behaved in general (the definition involves an existential quantifier, which is something complicated for automation), so if one can use preimages of sets instead this is often better. Here, you could use something like (hf : is_local_min_on f t (g b)) (hst : s ⊆ g ⁻¹' t).

view this post on Zulip Frédéric Dupuis (Jul 19 2020 at 20:19):

Ah, I see!

view this post on Zulip Frédéric Dupuis (Jul 19 2020 at 20:19):

OK, I'll PR the modified versions as soon as I manage to set up github properly...

view this post on Zulip Heather Macbeth (Jul 19 2020 at 20:31):

Just to check, you know about the handy tutorial at https://leanprover-community.github.io/contribute/index.html, right? There's a video version too :)

view this post on Zulip Frédéric Dupuis (Jul 19 2020 at 20:38):

Yes! I guess I am now at step 3, in which I am supposed to ask for write access on Zulip :-)

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 20:40):

What's your github username? :smiley:

view this post on Zulip Frédéric Dupuis (Jul 19 2020 at 20:40):

dupuisf

view this post on Zulip Bryan Gin-ge Chen (Jul 19 2020 at 20:40):

Done: https://github.com/leanprover-community/mathlib/invitations

view this post on Zulip Frédéric Dupuis (Jul 19 2020 at 20:41):

Thanks!

view this post on Zulip Scott Morrison (Jul 20 2020 at 01:19):

Sebastien Gouezel said:

Yes, this kind of lemma definitely makes sense for mathlib. One remark though about this one: images of sets are not really well behaved in general (the definition involves an existential quantifier, which is something complicated for automation), so if one can use preimages of sets instead this is often better. Here, you could use something like (hf : is_local_min_on f t (g b)) (hst : s ⊆ g ⁻¹' t).

Is this something we could write a linter to assist with? It's not obvious to new contributors that this should be preferred.

view this post on Zulip Heather Macbeth (Jul 20 2020 at 02:35):

In answer to this very question :smiley: :

Sebastien Gouezel said:

I don't think I like the linter idea, everyone should be free to make his own mistakes :-)

view this post on Zulip Scott Morrison (Jul 20 2020 at 02:58):

Oops, maybe now I remember you asking that, and thought it was a good idea, so asked again without remembering it had been answered!


Last updated: May 17 2021 at 16:26 UTC