Local vs global minimum

Stream: Is there code for X?

[Frédéric Dupuis]

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)?

[Yury G. Kudryashov]

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

[Frédéric Dupuis]

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

[Frédéric Dupuis]

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...?

[Frédéric Dupuis]

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))

[Sebastien Gouezel]

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).

[Frédéric Dupuis]

Ah, I see!

[Frédéric Dupuis]

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

[Heather Macbeth]

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 :)

[Frédéric Dupuis]

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

[Bryan Gin-ge Chen]

What's your github username? :smiley:

[Frédéric Dupuis]

dupuisf

[Bryan Gin-ge Chen]

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

[Frédéric Dupuis]

Thanks!

[Scott Morrison]

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.

[Heather Macbeth]

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 :-)

[Scott Morrison]

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