convex is supremum of affine

Stream: Is there code for X?

[Rémy Degenne]

I have a real convex function and I want to say that it is equal to a supremum of affine functions. Do we have this somewhere?

[Yaël Dillies]

There's some stuff in analysis.convex.function (and the next analysis file in the import tree) which looks like this, but I expect that we don't have it because how would you describe these affine functions? Is there a simpler way than going through derivation?

[Rémy Degenne]

I would be fine with a result about subgradients, but I think this could be obtained from convexity of the epigraph and results about supporting hyperplanes. But my memory is unclear on that point. I thought I saw some separation results in convexity PRs which could be related. I guess that I should first look for a proof, then look at which pieces of it are there. Thanks!

Also, in case I am not asking about the right thing: what I want to do is prove Jensen's inequality for the conditional expectation. The proof I would naturally write starts from the way the conditional expectation behaves on affine transformations of functions, hence writing convex functions using affine ones is useful. Maybe there is a better way of doing it, based on what we have about convexity.

[Rémy Degenne]

I found a source which does exactly what I want to do: I am looking for a version of theorem 2 of https://www.uio.no/studier/emner/matnat/math/MAT4410/h19/undervisningsmateriale/jensen.pdf

[Reid Barton]

If you don't need the countability, we probably already know that the convex hull of any $S$ is the intersection of all the half-spaces containing $S$. Now apply this to $S = \{\,(x, y) \mid y \ge f(x)\,\}$. It's pretty easy to see that any half-space containing $S$ has to be of the form $\{\,y \ge a(x)\,\}$ for some affine $a$, and then that $S$ is this intersection means exactly that $f(x)$ is the supremum of all the $a(x)$, I think.

[Patrick Massot]

I'm very happy to see this question because it means mathlib is moving in directions that we haven't explored yet.

[Yaël Dillies]

I assume you can say that's in the supremum of the affine functions which are less than it, and you get one direction directly, but I don't know how hard (and what generality is needed) is the other way.

[Reid Barton]

Do we know that a closed convex set is the intersection of the closed half-spaces containing it?

[David Wärn]

For countability, the argument in the pdf actually shows that if $f = \sup_{i \in I} f_i$ is a supremum of affine functions, then there is a countable $J \subseteq I$ such that $f = \sup_{i \in J} f_i$. You can just replace $f_x$ with a countable $I_x \subseteq I$ such that $f(x) = \sup_{i \in I_x} f_i(x)$.

[Yaël Dillies]

Reid Barton said:

Do we know that a closed convex set is the intersection of the closed half-spaces containing it?

I have that on a branch! Eidelheit's theorem.

[David Wärn]

I guess it's also true that a closed convex set is a countable intersection of half-spaces. (Basically the space of all half-spaces is second countable, so the subspace of supporting half-spaces is in particular separable)

[Yaël Dillies]

Here's the precise line where I proved Eidelheit's theorem: https://github.com/leanprover-community/mathlib/blob/sperner-again/src/combinatorics/simplicial_complex/exposed.lean#L69

[Yaël Dillies]

The only prerequisite is #7288