Weak compactness of closed balls in a reflexive Banach space

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

In one of my projects I would like to have the weak compactness of a closed ball in a Hilbert space. That is, I want a proof of the following theorem:

import Mathlib

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]

theorem isCompact_closedBall (r : ℝ) :
    IsCompact (⇑(toWeakSpace ℝ H) '' Metric.closedBall 0 r) := by
  sorry

The correct approach is probably to prove that a Banach space is reflexive iff its closed unit ball is weakly compact, and then show that a Hilbert space is uniformly convex and thus reflexive. We have IsReflexive, but I don't see the corresponding one for topological vector spaces. Is anyone working on some basic APIs for reflexive Banach spaces? I am happy to open a PR myself or help/collaborate with someone.

[Jireh Loreaux]

I don't have any work directly on reflexive Banach spaces, but I have recently been doing a lot of work on weak topologies and weak duals in a downstream repo. Among other things, I have a proof of the Krein-Smulian theorem which I will try to PR to Mathlib soon.

[Yongxi Lin (Aaron)]

@Jireh Loreaux Thank you for your response. In your downstream project, do you have any plan of generalizing ContinuousLinearMap.apply (at least to locally convex Hausdorff spaces)? Not sure why right now they are only defined for normed spaces, but I think this generalization is needed as reflexive space is defined by using ContinuousLinearMap.apply 𝕜 𝕜.

[Filippo A. E. Nuccio]

I have an open PR where I prove Millman-Pettis but it depends on the bipolar theorem that is currently under review. It is the main PR I'm working on but unfortunately this doesn't mean I've got a lot of time for it.

[Jireh Loreaux]

@Yongxi Lin (Aaron) sorry, I missed this. No, I'm not working on it.

[Jireh Loreaux]

@Filippo A. E. Nuccio have you taken over Christopher Hoskin's bipolar PR? I would be happy for you to do that (when you have the time, of course).

[David Gross]

Speaking of the bipolar PR, @Paradoxy and me have just posted #35422, which fixes up an auxiliary result (the "weak representation theorem") that's part of #26345.

[Filippo A. E. Nuccio]

Jireh Loreaux said:

Filippo A. E. Nuccio have you taken over Christopher Hoskin's bipolar PR? I would be happy for you to do that (when you have the time, of course).

This is what I'm planning to do starting on Monday, once a terrible deadline (due Sun) will finally be over.