Convex functions are continuous

Stream: maths

[Yaël Dillies]

For anybody interested, I have a draft of the fact that convex functions from a finite dimensional real inner product space to ℝ are continuous in #17081. The structure of the proof is already set up. What needs doing is filling in the details. In particular, I have trouble with proving continuity from the epsilon-delta definition because my candidate delta is possibly zero, but if you look at the argument (second answer here), you will that it should cause any trouble.

[Yaël Dillies]

Help wanted!

[Heather Macbeth]

The "inner product space" assumption seems odd. To generalize to normed space, perhaps you can observe that for vectors $v_1,\ldots v_N$ which span a finite-dimensional real normed space $V$, the map $\mathbb{R}^N\to V$ defined by $x\mapsto \sum_i x_iv_i$ is surjective and therefore open. So the "strict convex hull" of such points in $V$ is open, and so their convex hull is a neighbourhood of zero.

Relevant lemmas: docs#continuous_linear_map.exists_right_inverse_of_surjective, docs#is_open_map.of_sections

[Yaël Dillies]

That's the kind of generalisation I was after, thanks!

[Yaël Dillies]

Where is the fact that this function is surjective? Not sure what the mathlib way of spelling it out is.

[Yaël Dillies]

and do you have a better proof that ball 0 1 (in the ∞-metric) gets mapped to the convex hull of the parallelepiped than brute-forcing the convex combinations?

[Junyan Xu]

You may use docs#basis.equiv_fun with the basis produced by docs#finite_dimensional.fin_basis and then you know both direction are continuous (docs#linear_map.continuous_of_finite_dimensional) so it's a homeomorphism (you just need a Hausdorff TVS, not a norm).

I also suggest that you use a simplex instead of a hypercube; we have
0 = 1/(n+1) * (-1, -1, ..., -1) + 1/(n+1) * (1, 0, ..., 0) + 1/(n+1) * (0, 1, ..., 0) + ... + 1/(n+1) * (0, 0, ..., 1)
and since all coefficients are positive, we may solve easy equations to get a convex combination that sum up to any (small enough) (x1, x2, ..., xn).

[Yaël Dillies]

The good thing about using an hypercube is that I have access to lemmas like docs#convex_hull_prod (but the pi version, which I apparently forgot to write).

[Yaël Dillies]

I think that allows me to fully avoid touching linear combinations? All the heavy lifting is done by docs#Icc_subset_segment.

[Junyan Xu]

Yeah that lemma is pretty convenient and seems to solve all difficulties. I think you can then just use the ∞-metric on R^n, where balls are just set.pi of identical segments, and then transfer the result to any Hausdorff TVS; just amounts to composing the convex function with the bi-continuous linear_equiv, right?

[Yaël Dillies]

Something like that, yeah. But there's still a lot of glue missing in between.

[Yaël Dillies]

Right now, I am proving a bunch of properties of the hypercube inline, which doesn't sound great.

[Yaël Dillies]

I am done for today. I just pushed all I have so far and ecnourage anyone to have a look at the seven sorries. None of them is hard, but they sure make me grit my teeth.

[Antoine Chambert-Loir]

@Yaël Dillies , take a good book on convex analysis where the mathematical proof is clear.
One I like is Hiriart-Urruty, Convex Analysis and Optimization. The proof is pages 173--.

[Antoine Chambert-Loir]

I copy the three relevant pages
image.png
image.png
image.png

[Heather Macbeth]

You can probably get the surjectivity working with the simplex using docs#affine_basis.surjective_coord

[Yaël Dillies]

Oh no, I was trying to avoid the relative interior and here it comes again :rofl:

[Yaël Dillies]

@Paul A. Reichert, how are relative things going?

[Paul A. Reichert]

Yaël Dillies said:

Paul A. Reichert, how are relative things going?

Oh, I was pushing my code in small PR tranches and then I got sidetracked by the time-intensive weeks before my Master's thesis deadline Thursday, October 27th. After that, I'll continue with the merging work, I promise :)

[Paul A. Reichert]

Update: I've picked up where I left a few days ago. I was breaking down my code into smaller PRs and now I have to change some parts of the module about the intrinsic interior to accomodate the changes introduced during code review. So -- I'm not exactly finished but working on it. The main work is extracting the required linear algebra lemmas and PRing them in small pieces.