Hahn-Banach separation in TVS

Stream: general

[Anatole Dedecker]

Just wanted to point out that I just opened #16796 which generalizes the whole analysis/normed_space/hahn_banach/separation file to general topological vector spaces (with suitable local convexity hypotheses). Adapting the proofs was actually pretty straightforward once all the preliminaries were set up (thanks to @Bhavik Mehta and @Yaël Dillies!), but I think this is the first big functional analysis theorem that we prove in a non-normed context, so I'd say it's a nice milestone!

The next target in this direction is the general Banach-Steinhaus theorem, which is actually what motivated me to work on this generalization. This will allow us to get the uniform boundedness principle for distributions @Moritz Doll

[Yaël Dillies]

That's great! It's the generality I wanted it in but it wasn't available at the time of writing.

[Jireh Loreaux]

I'm excited! I did Banach-Steinhaus almost a year ago only for normed spaces, so it will be a nice upgrade!

[Junyan Xu]

Another target would be to generalize Krein-Milman if people want to develop ergodic theory (usually we want compactness in the weak* topology).

[Anatole Dedecker]

I did it in the same PR because it’s just changing the hypotheses :upside_down:

[Anatole Dedecker]

Unless you are talking about a stronger generalization

[Yaël Dillies]

Ahah, I was about to open a PR depending on yours to generalize KM.

[Anatole Dedecker]

The thing is the linter was complaining, because the Krein-Milman file doesn't import analysis/locally_convex/with_seminorms, so it didn't know yet that a normed space is locally convex. But I thought it was dumb to add it as a dependency only to remove it in a later PR, especially since the "generalization" really just involves changing the assumptions (again, except if you are thinking about a stronger sense of "generalization")

[Yaël Dillies]

No, I meant that generalisation indeed!

[Junyan Xu]

Yeah thanks I think it's now at least as general as the Wikipedia statement. Though I think we still have a stronger result to aim for, which is used for ergodic decomposition.

[Yaël Dillies]

Yeah, I had plans to do Choquet theory this summer, but my summer project took over :neutral:

[Anatole Dedecker]

Yaël Dillies said:

Ahah, I was about to open a PR depending on yours to generalize KM.

If you (or anyone else) want to have fun with this version of Hahn-Banach, something that would be helpful is the bipolar theorem. To prove equivalence between different characterizations of barrels, I will have to prove some special case of it, but I probably won't take the time to prove the full theorem. But it anyone wants to work on that, it would make my proof cleaner!

[Filippo A. E. Nuccio]

Something like this? In which form do you need it, actually?

[Anatole Dedecker]

What I need is that a closed (for the original topology, no weak things in my case) convex set containing 0 is equal to its bipolar

[Filippo A. E. Nuccio]

And this for an arbitrary locally convex TVS? I have looked at your PR, can you point out at where you would like to use it (so that I can check the exact assumptions you would like to work under)?

[Moritz Doll]

the bipolar theorem should not be that hard, one probably needs some facts about the disked hull (convex hull of the balanced hull), but all the basics for that should have been done.

[Filippo A. E. Nuccio]

I would like to go for it, indeed. I was just wondering with @Anatole Dedecker about the setting he had in mind.

[Anatole Dedecker]

Oh yes sorry, I had things to do yesterday evening, I’ll write about what I need precisely as soon as my lecture ends

[Filippo A. E. Nuccio]

No problem!

[Anatole Dedecker]

Okay so let's consider the three following statements:

import analysis.normed_space.hahn_banach.separation
import analysis.locally_convex.polar

variables {𝕜 E F : Type*} [normed_field 𝕜] [normed_space ℝ 𝕜]
  [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F]
  [module ℝ E] [module ℝ F]
  [is_scalar_tower ℝ 𝕜 E] [is_scalar_tower ℝ 𝕜 F]
  [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E]
  [topological_space F] [topological_add_group F] [has_continuous_smul ℝ F]
  {s : set E}

lemma A [locally_convex_space ℝ E] (hs₀ : (0 : E) ∈ s) (hs₁ : convex ℝ s) (hs₂ : is_closed s) :
  (top_dual_pairing 𝕜 E).polar ((top_dual_pairing 𝕜 E).flip.polar s) = s :=
sorry

lemma B {p : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} :
  p.flip.polar (p.polar s) = @@closure (weak_bilin.topological_space p) (convex_hull ℝ (s ∪ {0})) :=
sorry

lemma C [locally_convex_space ℝ E] :
  (top_dual_pairing 𝕜 E).polar ((top_dual_pairing 𝕜 E).flip.polar s) = closure (convex_hull ℝ (s ∪ {0})) :=
sorry

What I need is A, which I can prove directly using the Hahn-Banach separation theorem. But the "morally correct" way to do it is to prove B (which is the "true" bipolar theorem) using Hahn-Banach (because the weak topology is always locally convex), then deduce C using Hahn-Banach again to say that weakening topologies doesn't change convex closed sets, and finally A follows trivially from C.

[Filippo A. E. Nuccio]

Oh great, that's clear (and nice!). I will see if I can find time soon to open a PR with your skeleton of proof, and if yes I will mention it in this chat.

[Anatole Dedecker]

Note that I probably won't go back to this for two weeks because I'll focus on keeping all my open PRs up to date while preparing for my midterms

[Anatole Dedecker]

Filippo A. E. Nuccio said:

Oh great, that's clear (and nice!). I will see if I can find time soon to open a PR with your skeleton of proof, and if yes I will mention it in this chat.

Nice, thanks!

[Moritz Doll]

@Anatole Dedecker you are aware of the fact that we have different polar than Bourbaki? I am not sure whether your statements are correct for the mathlib definition of the polar. For instance our polar should be balanced, but the RHS of B does not look balanced to me.

[Anatole Dedecker]

Ah right, I forgot about that. I had checked that it didn’t matter in my case, because s is also balanced (it’s a barrel), so my brain somehow got rid of that information

[Anatole Dedecker]

So I guess to get a correct statement we just have to add the hypothesis that s is balanced in A, and then consider the intersection of all closed balanced sets containing s instead of the closed convex hull of s \union {0} in B and C. Does that sound right? And IIUC this smallest closed balanced convex set is exactly the closure of the disked hull you mentioned above, right?

[Moritz Doll]

yes, replace $s \cup \{0\}$ by $\operatorname{cobal}(s)$, in A you probably have to add balanced if you want to have s on the RHS.

[Moritz Doll]

Narici-Beckenstein use the absolute polar, so their version of the bipolar theorem should have the correct assumptions (the proofs in that book are a bit weird, but the statements are correct as far as I have seen)