WIP

PR summary b72c03457b

Import changes for modified files

No significant changes to the import graph

Declarations diff

+ iInter_countable_halfSpaces_eq
+ iInter_halfSpaces_eq'

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

./scripts/reporting/technical-debt-metrics.sh pr_summary

This pull request has conflicts, please merge master and resolve them.

-WIP

-awaiting-author

This pull request has conflicts, please merge master and resolve them.

-awaiting-author

What do you think about the following alternative approach? I'm not sure it works (I just made it up).

Thanks to SecondCountableTopology.toHereditarilyLindelof, E is hereditarily Lindelöf.

This implies that the complement sᶜ of your convex set is Lindelöf.

Now, you know by RCLike.iInter_halfSpaces_eq (or a variation of it) that s can be written as a huge intersection of closed halfspaces. In other world, the intersection of all these hyperplanes with sᶜ is empty. But then, IsLindelof.elim_countable_subfamily_closed gives you a countable subfamily which satisfies the same thing, hence you are done.

Even cleaner: you can prove and use the dual version of eq_open_union_countable.

@ADedecker Thank you for your comments. I updated my PR and here's a quick summary: I proved that if s is a closed convex set in a locally convex TVS E such that its complement is Lindelof, then it is equal to an intersection of countably many half spaces. The assumption is a bit weird, but it applies to an arbitrary convex closed set in a HereditarilyLindelof locally convex TVS.

-awaiting-author

This pull request has conflicts, please merge master and resolve them.

Sorry, I really did not want to block this for so long... Whenever you are waiting for a response from the reviewers, feel free to remove "awaiting-author" tag, otherwise your PR will probably be overlooked...

I've thought a bit about your application, and this led me to #33778 (found in Bourbaki): this tells you that, as long as the domain is hereditarily Lindelof, if you know how to write your function as an arbitrary supremum of some lower-semicontinuous functions, then you can actually restrict to a countable subfamily without changing the supremum.

I claim the right approach is thus to prove the more general result that, in a locally convex space E, any convex lower-semicontinuous function φ : E → ℝ is an uncountable supremum of continuous affine functions. This is a more general result, and I think the proof is also simpler because you don't have to worry about countability. How does this sound?

Note that the content of this PR is still relevant, even if it might not be used for the final approximation result.

@ADedecker Thank you for you reply. I was procrastinating because I was unsure about whether I should include the existence of nonzero linear forms in this PR. #33778 is great but I think it still can't resolve this problem. I am using https://link.springer.com/book/10.1007/978-3-319-48520-1 as my reference (the proof that a convex lower semicontinuity function is supremum of countably many affine functions is in Lemma 1.2.10, but I believe countability is not really used anywhere in that lemma, so the same proof works for the uncountable case), and I still believe the existence of nonzero linear forms is necessary (at least in the proof of Lemma 1.2.10, although it is not clearly written in the book).

I am happy to change my code if you have a reference of a better proof, and I think it is probably better to continue our discussion on Zulip: #mathlib4 > Discussion thread for Conditional Jensen's Inequality

This pull request has conflicts, please merge master and resolve them.

• awaiting-author

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step