## Stream: Is there code for X?

### Topic: Local vs global minimum

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

#### Yury G. Kudryashov (Jul 18 2020 at 15:38):

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

#### Frédéric Dupuis (Jul 18 2020 at 17:46):

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

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

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


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

Ah, I see!

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

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

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

dupuisf

Thanks!

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

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

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