Finite Dimensional Convex Functions are Locally Lipschitz

Stream: mathlib4

[Zichen Wang]

Hi,

Here's Zichen Wang.

I am currently seeking the permission to create a new branch where we can contribute our formalized codes to Mathlib.  And I would like to make PRs.

My Github username : imathwy

I have proved that each convex function on an open convex subset of FiniteDimensional space is locally Lipschitz continuous, so that continuous.

[Yaël Dillies]

Hey! Thanks for offering but have you seen #14999 ?

[Zichen Wang]

Yaël Dillies 发言道：

Hey! Thanks for offering but have you seen #14999 ?

May I ask if you have already proved it?

[Yaël Dillies]

Feel free to add your proof to #14999. The current status is that I am waiting on the convexity refactor (search on Zulip for what I mean) to prove the stronger statement that ConvexOn ℝ s → LocallyLipschitzOn (intrinsicInterior ℝ s).

[Yaël Dillies]

I assume you have proved ConvexOn ℝ univ f → LocallyLipschitz f

[Zichen Wang]

Yaël Dillies 发言道：

I assume you have proved ConvexOn ℝ univ f → LocallyLipschitz f

I have prove this:
(hs_convex : Convex ℝ s)(hs_isopen : IsOpen s)(hf : ConvexOn ℝ s f)
    : LocallyLipschitzOn s f

[Zichen Wang]

This is my first PR and I need your help , what should I do next?

[Yaël Dillies]

Can @maintainers give imathwy mathlib access on github?

[Zichen Wang]

Thank u

[Yaël Dillies]

@Eric Wieser in particular, my above PR is still waiting on #14660

[Floris van Doorn]

Mathlib invite sent

[Zichen Wang]

Floris van Doorn 发言道：

Mathlib invite sent

Thank u .I got it.

[Zichen Wang]

QQ_1724286810841.png
May I ask how this problem can be solved?

[Bryan Gin-ge Chen]

You can ignore that; it doesn't have to do with Lean code at all.

[Zichen Wang]

QQ_1724287061773.png
But when I PR , it said Some checks were not successful

[Bryan Gin-ge Chen]

It looks like you're working on #16038. If so, you should close that PR and open a new one from a new branch in the mathlib4 repo. Please see the instructions here: https://leanprover-community.github.io/contribute/index.html

[Zichen Wang]

Bryan Gin-ge Chen 发言道：

It looks like you're working on #16038. If so, you should close that PR and open a new one from a new branch in the mathlib4 repo. Please see the instructions here: https://leanprover-community.github.io/contribute/index.html

Thank u.Let me try it

[Zichen Wang]

QQ_1724294546813.png
Is the next thing I should do only to wait it to be reviewed by administrator?

[Yury G. Kudryashov]

If your PR is on the #queue (probably, near the last page now), then it's time to wait for a review.

[Yaël Dillies]

Also please add your result to #14999. No need to open a new PR

[Zichen Wang]

Yaël Dillies 发言道：

Also please add your result to #14999. No need to open a new PR

OK，let me try.But I have opened a new PR.Should I close it ?

[Zichen Wang]

I have added it to #14999. You can check it

Yaël Dillies 发言道：

Also please add your result to #14999. No need to open a new PR

[Yaël Dillies]

I see. Can you golf your proof using my template proof?

[Yaël Dillies]

You will need to use the result I am proving in #14660 (which is also available in #14999)

[Zichen Wang]

Yaël Dillies 发言道：

I see. Can you golf your proof using my template proof?

Does it mean that I finish that theorem of yours (statement that ConvexOn ℝ s → LocallyLipschitzOn (intrinsicInterior ℝ s).) by using my conclusion?

[Yaël Dillies]

Nono.

1. You can't quite prove ConvexOn ℝ s → LocallyLipschitzOn (intrinsicInterior ℝ s) before I'm done with the convexity refactor (this is going to take a while)
2. You should instead look at how I started the proof in Analysis.Convex.Continuous

[Yaël Dillies]

Actually I don't see that file in the PR, but here it is: https://github.com/YaelDillies/LeanCamCombi/blob/48d5ded0cf6c9565036b14bdaedc1eeea23510c9/LeanCamCombi/ConvexContinuous.lean

[Zichen Wang]

To be honest,I am confusing what I should do. Does it mean that I should add my result in Analysis.Convex.Continuous?

[Yaël Dillies]

I mean that your proof is not very efficient since it reproves the result from #14660 in a hidden way. If you manage to leverage the result in #14660, you can shorten your proof two-fold

[Zichen Wang]

Yes,you're right. I'll try it.

[Zichen Wang]

If I use the lemma  exists_mem_interior_convexHull_affineBasis  , the file "l1space" is no longer needed and it's quite simplified. You can check it :grinning_face_with_smiling_eyes:

[Yaël Dillies]

Yes indeed it is a lot nicer!

[Zichen Wang]

By the way , I have tried to prove the more general thm (statement that ConvexOn ℝ s → LocallyLipschitzOn (intrinsicInterior ℝ s) by my thm. But the problem is like failed to synthesize AddCommMonoid ↥(affineSpan ℝ s). Is it what you are doing?

[Yaël Dillies]

Yes, this is what I am fixing indeed

[Zichen Wang]

If these problems can be solved , the  general thm (statement that ConvexOn ℝ s → LocallyLipschitzOn (intrinsicInterior ℝ s) can be proved easily by my thm.

[Yaël Dillies]

@PrinChern, I have now finished cleaning up your proof and incorporating it into my file. I will now open a few prerequisite PRs. Expect it to take 2-3 weeks before #14999 itself is merged.