Discussion thread for Conditional Jensen's Inequality

Stream: mathlib4

[Yongxi Lin (Aaron)]

This is the discussion thread for my PR of conditional Jensen's inequality: #27953. This is also my first project :) (which I received a lot of help from @Thomas Zhu ). Feel free to give me some suggestions on how I can improve this PR here.

[Yongxi Lin (Aaron)]

This PR is long, and I divided it into several pieces:#31180, #31399, #31411. Right now only #31399 was merged into Mathlib (and hopefully more in the future).

An essential lemma used in this proof is to write a convex lower semicontinuous function as the supremum of a collection of countably many affine function (#31399), and this relies on writing a closed convex set s as the intersection of a collection of countably many halfspaces (#31180). #31180 is also what I want to focus on in this thread right now. I was stuck at #31180 because I was unsure about a question raised by my reviewer @Anatole Dedecker : is it necessary to include the statement that the halfspaces are generated by nonzero linear forms when s is not empty?

I believe this is still kind of necessary (at least in the proof of my reference: Lemma 1.2.9 and Lemma 1.2.10 of https://link.springer.com/book/10.1007/978-3-319-48520-1). I am happy to change my code if anyone have a better reference for this result.

[Anatole Dedecker]

Sorry I indeed forgot part of the story in my last comment of the PR. Here are some more precise thoughts:

• regarding requiring non-zero linear forms, I retract my initial scepticism: geometrically it does make a ton of sense to specialize to non-zero linear forms, because they correspond/define hyperplanes.

• regarding #31411, I suggested using #33778 to take care of the countability. The nice thing about the general version (general LCTVS, no countability) is that it's actually easier to prove sice you don't care about countability! You may find such a proof in Bourbaki, Topological Vector Spaces, § 5, Prop. 5. Notice how you're doing the approximation at each point, which is completely undoable if you try to take care of countability too early.

[Anatole Dedecker]

Re: nonzeroness. I think I would find the results more satisfying it the case disjunction was based on triviality of E rather than emptiness of s: as soon as E is nontrivial, even the emptyset may be written as an intersection of non-degenerate closed half-spaces. And one can often get a Nontrivial instance on E by doing nontriviality E. Does that make sense?

[Anatole Dedecker]

To sum up, here is what I envision:

• I think you should prove #31411 using the general non-countable approximation result, and getting countability from #33778
• I still think the results from #31180 are interesting. I claim that they should be written in a slightly more "canonical" way. I will write these down tomorrow.

[Anatole Dedecker]

(Sorry I had mixed some PR numbers. Should be fixed now)

[Yongxi Lin (Aaron)]

@Anatole Dedecker I was a bit busy with my other commitments recently. I will try my best to take a look of your comments more closely later this week.