2 Locally Convex and Bolognese Spaces

In this chapter, all Banach spaces are supposed to be non-zero. Observe that the definition BanachSpace does not exist in Mathlib: before starting off, make sure that you know how to state that a space \(V\) is Banach.

2.1 Duals of Banach Spaces

Theorem 2.1

✓

If \(V\) is a Banach space and \(v\neq 0\), then some \(\varphi \in V^*\) satisfies \(\varphi (v) \neq 0\).

Proof ▶

The result is in Mathlib verbatim, the problem is to find it.

Suggestion : prove first the separation result 2.2.

Theorem 2.2

✓

Let \(V\) be a Banach space and let \(v\neq w\neq w\) be two distinct elements of \(V\). There is a \(\varphi \in V^*\) such that \(\varphi (v) \neq \varphi (w)\).

Proof ▶

See the proof of Theorem 2.1. Extra questions: Are you sure that completeness is necessary?

2.2 Bolognese Spaces

Definition 2.3

✓

A topological vector space is Bolognese if the convex open sets are a base for the topology: for every open set \(U\) around a point, there is a convex open set \(C\) containing that point such that \(C\subseteq U\).

The above definition is almost identical to the definition of Locally Convex Space of Mathlib.

Theorem 2.4

✓

A topological vector space is Bolognese if and only if it is Locally Convex.

Proof ▶

The proof consists in unfolding the definition of a basis of a topological space, using that when \(V\) is a topological vector space (so, addition and scalar multiplications are continuous), there is a basis of the neighborhoods of \(0\) made of open, absolutely convex spaces (this is in Mathlib).

Theorem 2.5

✓

Every Banach space is Bolognese.

Proof ▶

Since Banach spaces are locally convex, this follows from Theorem 2.4. On the other hand, completeness is probably useless: try to generalise.

Theorem 2.6

✓

For every \(1\le p\) the space \(L^p([0,1])\) (where \([0,1]\) is endowed with the restriction of the Lebesgue measure) is Bolognese.

Proof ▶

All the ingredients are in Mathlib: the only “problem” is how to state the theorem, namely how to speak about \(L^p([0,1])\).

Finally, we see that Theorem 2.2 was a special case of a more general result:

Theorem 2.7

✓

Let \(V\) be a Hausdorff Bolognese space and let \(v\neq w \in V\) be distinct elements of \(V\). There is a \(\varphi \in V^*\) such that \(\varphi (v) \neq \varphi (w)\).

Proof ▶

Once more, the proof is basically a matter of finding the right formulation and right statement in Mathlib. Observe (i. e.: try!) that you can assume T1 instead of Hausdorff, if you so wish.

2.3 Non-Bolognese Spaces

It comes the question of understanding whether every space is Bolognese and, if not, to produce examples of non-Bolognese ones.

Theorem 2.8 Tychonoff (1935), see [

✓

For every \(0{\lt}p{\lt}1\), the space \(\ell ^{p}\) of sequences \((x_n)_{n\in \mathbb {N}}\) of real numbers such that \(\sum _{n\geq 0}\lvert x_n\rvert ^p {\lt} \infty \) is not Bolognese.

Proof ▶

Arguing by contradiction, suppose that the unit ball \(\mathcal{B}(0,1)\subseteq \ell ^p\) contains a convex open \(0 \ni U\subseteq \mathcal{B}(0,1)\): then \(U\) contains a ball \(\mathcal{B}(0,\varepsilon )\) for some \(\varepsilon \).

For each \(1\le i\le \infty \), let \(x_i=(\varepsilon \delta _{i,j})_{j}\) be the vector whose coordinates are \(0\) at all \(j\ne i\) and whose \(i\)-th coordinate is \(\varepsilon \): clearly, \(x_i\in \mathcal{B}(0,\varepsilon )\subseteq \ell ^p\). Consider now, for each \(N\in \mathbb {N}\), the vector

\[ y_N = \sum _{i=1}^N \frac{1}{C_N\cdot i^{1/p}}x_i = \bigr(0,\dots ,\frac{\varepsilon }{C_Ni^{1/p}}\bigl) \]

where \(C_N=\sum _{i=1}^N i^{1/p}\). Clearly all \(y_N\) are (finite) linear combinations of the \(x_i\)’s, so they all belong to the convex set \(U\subseteq \mathcal{B}(0,1)\). On the other hand,

\[ \Vert y_N\Vert = \sqrt[p]{\left(\sum _{i=1}^N \frac{\varepsilon }{C_N\cdot i^{1/p}}\right)^p} = \sqrt[p]{\sum _{i=1}^N \lvert (\frac{\varepsilon ^p}{C_N^p\cdot i}\rvert )} = \frac{\varepsilon }{C_N}\sqrt[p]{\sum _{i=1}^N \frac{1}{i}}. \]

Now, since

\[ \lim _{N\to +\infty }\frac{1}{\sum _{i=1}^N \sqrt[p]{i}}\sqrt[p]{\sum _{i=1}^N \frac{1}{i}} = \lim _{N\to +\infty }\frac{1}{\sum _{i=1}^N \sqrt[p]{i}}\sqrt[p]{\sum _{i=1}^N \frac{1}{i}} = +\infty \]

there exists \(N\) such that \(\Vert y_N\Vert {\gt} 1\), contradicting the assumption that \(y_N\in \mathcal{B}(0,1)\) for all \(N\).

Passing from numerical sequences to measurable functions yields other examples:

Theorem 2.9

✓

For every \(0{\lt}p{\lt}1\), the space \(L^{p}([0,1])\) of equivalence classes of measurable functions \(f\colon [0,1]\to \mathbb {R}\) satisfying \(\int _0^1\lvert f(x)\rvert ^{p}\mathrm{d}x {\lt} \infty \) (with respect to the Lebesgue measure) is not Bolognese.

Proof ▶

Combine Theorem 2.10 and Theorem 2.7.

The above theorem can be proven directly, but we rather deduce it as a corollary of the following one, combined with Theorem 2.7:

Theorem 2.10

✓

For every \(0{\lt}p{\lt}1\) the dual space \(L^p([0,1])^\ast \) is equal to \(0\).

Proof ▶

For a direct proof, see [ .