Sequential version of Banach-Alaoglu

Stream: Is there code for X?

[Etienne Marion]

Hi! I see that Banach-Alaoglu theorem (docs#WeakDual.isCompact_closedBall) is in Mathlib. It states that the closed balls of the continuous dual space of normed space X are compact for the weak-star topology. Do we have the sequential version of this? That is, if the space X is separable, then the closed balls are sequentially compact (in fact the weak-star topology on the closed balls in metrizable in this case).

[Yaël Dillies]

@Janette Setälä just finished proving the sequential Banach-Alaoglu!

[Etienne Marion]

Oh nice! Is it in a PR yet?

[Yaël Dillies]

No, but the plan is to get it PRed this week

[Etienne Marion]

It's all right I don't need straight away, but that's cool! Thanks for your answer.

[Jireh Loreaux]

I thought we already had metrizability of the closed unit ball in the dual (in the weak⋆ topology) of a separable space. Am I wrong about that?

[Jireh Loreaux]

Hmmm.... seems not.

[Kalle Kytölä]

Indeed, Janette's proof goes via metrizability (as is natural). I don't think we had it before.

[Jireh Loreaux]

I'm curious about the API here (or rather, what @Janette Setälä is adding to it). It seems we're missing some. For instance, we should have something that says one docs#SeminormFamily is smaller than another (not just in terms of the actual elements). And then something like: if we have docs#WithSeminorms for some SeminormFamily, and this is smaller than another one (with respect to which all the seminorms are continuous), then we also have have docs#WithSeminorms for the larger one (or something to this effect).

[Janette Setälä]

Currently, both the Banach Alaoglu and the sequential version only work for a single norm.