Continuity of convex functions

Stream: maths

[Chenyi Li]

I am working on some properties of convex functions. I noticed that there was a discussion about the continuity of convex functions in this chat. I wonder what have been done about this. Specificlly, can we prove that in finite dimesional space, the convex function is locally Lipschitz continuous at the interior point. If we have this theorem, we can directly get that in finite dimensional space, if a function is convex over the entire space, then it is continuous or locally Lipschitz. We can find the theorem in the book first-order-methods-in-optimization as
pic.png
Thank you very much for joining in this discussion.

[Yaël Dillies]

Hey! It's basically done in LeanCamCombi. The only gap is to show that any point has a basis of neighborhoods made of polytopes

[Yaël Dillies]

Dumbing it down: If I give you an open set U and a point x ∈ U, find a finite set s ⊆ U such that x ∈ convexHull ℝ s

[Yaël Dillies]

If you can prove this, then we have a full proof

[Chenyi Li]

I will check it there, thank you!

[Ziyu Wang]

I think one possible solution is to make induction on the dimension of the space, is this possible?

[Yaël Dillies]

Maybe? You will probably need docs#intrinsicInterior then

[Yaël Dillies]

Here is the lemma I stated above: https://github.com/YaelDillies/LeanCamCombi/blob/master/LeanCamCombi/ConvexContinuous.lean#L54-L57

[Ziyu Wang]

Thanks,Thank you. I've been busy with other tasks at hand lately, but I'll try to make time to deal with this matter.
Regarding covering a neighborhood of a point with the convex hull of a finite number of points, my thoughts are as follows:

image.png

[Yaël Dillies]

Regarding the first line: The vector space might not be endowed with a metric. Of course everything is finite-dimensional so you can just wish a metric into existence, but that will probably be painful

[Yaël Dillies]

Yaël Dillies said:

any point has a basis of neighborhoods made of polytopes

@Anatole Dedecker, how would you state this? I'm at loss in the sea of IsTopologicalBasis and FilterBasis.

[Anatole Dedecker]

Something like this:

def foo {𝕜 E : Type*} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E]
    [TopologicalSpace E] : Prop :=
  ∀ x : E, (𝓝 x).HasBasis (fun s : Finset E ↦ convexHull 𝕜 s ∈ 𝓝 x) (fun s ↦ convexHull 𝕜 s)

[Anatole Dedecker]

Using docs#Filter.HasBasis

[Anatole Dedecker]

I guess it's also equivalent to the set of interiors of polytopes being a topological basis, but I'd say that's not a good choice given the amount of API we have for Filter.HasBasis.

[Yaël Dillies]

I assume ∀ x : E, (𝓝 x).HasBasis (fun s : Finset E ↦ convexHull 𝕜 s ∈ 𝓝 x) (↑) is a more direct translation of my statement?

[Anatole Dedecker]

I don't think so, this last coercion is the one from Finset to Set right?

[Yaël Dillies]

Yes. Why would it be incorrect?

[Anatole Dedecker]

Well with this version we would have that {-1, 1} is a neighborhood of 0 since its convex hull is ?

[Anatole Dedecker]

I think you mean ∀ x : E, (𝓝 x).HasBasis (fun s : Set E ↦ s ∈ 𝓝 x ∧ ∃ F, s = convexHull 𝕜 F) id