Banach–Alaoglu theorem

Stream: Is there code for X?

[Adam Topaz]

Dear functional analysts of mathlib --
How far are we from having the Banach–Alaoglu theorem? I'm not at all familiar with the functional analysis part of mathlib, but it seems that we have at least some of the necessary lemmas, e.g. docs#continuous_linear_map.is_closed_image_coe_closed_ball

[Moritz Doll]

We have it for normed spaces: docs#continuous_linear_map.is_compact_image_coe_closed_ball

[Adam Topaz]

Ha! just the lemma below :)

[Moritz Doll]

for topological vector spaces we are not that far, but as far as I know nobody is working on it

[Adam Topaz]

Thanks I'll try to see if I can use this in my use case

[Adam Topaz]

The issue is that the norm on the weak dual I am using is not the usual one, so I'm not completely sure it would work.

[Adam Topaz]

Actually, do we know that the weak dual is a closed as a subset of the cartesian product?

[Adam Topaz]

More precisely, I'm working with a normed space $V$ over $\mathbb{R}$ and looking at its weak dual $Hom(V,\mathbb{R})$.

[Jireh Loreaux]

I'm not sure what your topology is on that second space.

[Adam Topaz]

Just the product topology.

[Adam Topaz]

Namely I'm just looking at the map $Hom(V,\mathbb{R}) \to \prod_{v \in V} \mathbb{R}$.

[Adam Topaz]

And $Hom(V,\mathbb{R})$ has the weak topology

[Jireh Loreaux]

I think docs#weak_bilin.coe_fn_continuous should get you where you want to go, but I'm not at my machine right now.

[Adam Topaz]

Oh, continuity is easy to prove, but I think this is actually a closed immersion, and that's what I'm after.

[Jireh Loreaux]

docs#weak_bilin.embedding?

[Adam Topaz]

that's not a closed embedding, unfortunately :(

[Jireh Loreaux]

Sorry, out of time, I'm headed into a meeting. If this is still unanswered in a few hours I'll try to do it.

[Adam Topaz]

No rush! Thanks for the help :)

[Anatole Dedecker]

Wait is that really true? That would mean that a pointwise limit of continuous linear functionals is linear (which is trivial: docs#linear_map_of_tendsto) and continuous (which is false in general I believe). That would work if V is complete though, thanks to docs#continuous_linear_map_of_tendsto

[Adam Topaz]

Yes you're right. Fortunately, I'm in a situation with V being complete (alternatively, I'm happy to use just the algebraic dual in my particular context, since I have another way of restricting to continuous functionals).

[Jireh Loreaux]

docs#continuous_linear_map_of_tendsto is about sequences (actually, it could generalize to pointwise bounded families tending to some function pointwise), but the weak⋆ topology isn't first countable, so sequences won't be enough.

Adam, what statement do you need exactly? After Anatole's comment and a few minutes thinking about it, I'm not sure this is a closed immersion. However, your mention of Banach-Alaoglu at the beginning of the thread makes me suspect you only need something weaker. For example, if you just need to know that the unit ball of the dual is closed (in the product topology), then that's much easier, and this is a thing which comes up commonly in functional analysis.

[Adam Topaz]

Here is the precise situation -- I have a compact Hausdorff totally disconnected space $X$, and I'm considering $C(X,\mathbb{R})$ with the sup norm.
I'm looking at the weak dual $M = Hom^{cont}(C(X,\mathbb{R}),\mathbb{R})$. Choose some $p \in (0,1]$ and consider the set $M_{\le c}$ of all $f \in M$ such that $\sum_i |f(1_{U_i})|^p \le c$ where $1_{U_i}$ is the indicator function on $U_i$ and $U_i$ form a clopen partition of $X$. What I'm trying to show is that $M_{\le c}$ is compact. It's not quite a closed ball in the usual sense, but as far as I can tell it is indeed a closed subset which is bounded in the usual sense by $c^{1/p}$.

This is needed for one of the final examples we're trying to do for LTE.

[Adam Topaz]

So in some sense I would like to use docs#weak_dual.is_compact_of_bounded_of_closed to prove compactness of this $M_{\le c}$.
Is this a sound strategy? I'm not at all a functional analyst ;-/

[Adam Topaz]

If you have some other way to show that the functor sending a profinite space $X$ to the space of $p$-signed Radon measures bounded by $c$ commutes with cofiltered limits, then I'm all ears :)

[Jireh Loreaux]

To show this is compact in the product topology, the steps are:

1. Show that it is bounded in the norm topology on the dual and closed in the weak⋆ topology, both of which seem doable.
2. apply docs#weak_dual.is_compact_of_bounded_of_closed to get that it is compact in the weak⋆ topology
3. apply docs#weak_bilin.coe_fn_continuous to get that the image (under the "identity" function) is compact in the product topology. (this is why I originally mentioned this result, because I thought you wanted something to this effect.)

[Jireh Loreaux]

In other words, yes, your approach seems reasonable, but I did not check the viability of (1) carefully.

[Adam Topaz]

I'm quite sure I have a path forward with (1).

[Adam Topaz]

Thanks for the help! Even just discussing this out loud is helpful for me :)

[Moritz Doll]

@Jireh Loreaux do you really mean docs#weak_bilin.coe_fn_continuous or do you rather mean docs#weak_bilin.embedding ?

[Adam Topaz]

Just to clarify, I don't actually need to map to the product topology, so I think just (1) and (2) would suffice for my application.

[Jireh Loreaux]

Moritz, continuity suffices right? I mean, continuous images of compact sets are compact, so I don't think you would need it to be an embedding (although it is nevertheless in this case).

[Moritz Doll]

yes, of course. I was misinterpreting the map (and the docstring for docs#weak_bilin.embedding wrote the map as I wanted to see it).

[Jireh Loreaux]

I know, I had to think about it too when I first read it.

[Moritz Doll]

maybe I should add another docstring to docs#weak_bilin.coe_fn_continuous

[Jireh Loreaux]

cc @Kalle Kytölä I thought you might want to see Adam using your work on Banach-Alaoglu for normed spaces. See, it's useful even though it's not in full generality!

[Jireh Loreaux]

Moritz, while you're at it, there's no embedding specific to docs#weak_dual, whereas there does exist docs#weak_dual.coe_fn_continuous. If you think it's worth it, you could add the embedding too.

[Adam Topaz]

Quick update: The strategy (1) + (2) above worked perfectly :) See
https://github.com/leanprover-community/lean-liquid/blob/7284f07b6f14019d5cf7ebd7134fe9648b80bf47/src/examples/Radon/main.lean#L173

Thanks all for the help!