# Documentation

Mathlib.Analysis.LocallyConvex.Barrelled

# Barrelled spaces and the Banach-Steinhaus theorem / Uniform Boundedness Principle #

This files defines barrelled spaces over a NontriviallyNormedField, and proves the Banach-Steinhaus theorem for maps from a barrelled space to a space equipped with a family of seminorms generating the topology (i.e WithSeminorms q for some family of seminorms q).

The more standard Banach-Steinhaus theorem for normed spaces is then deduced from that in Analysis.NormedSpace.BanachSteinhaus.

## Main definitions #

• BarrelledSpace: a topological vector space E is said to be barrelled if all lower semicontinuous seminorms on E are actually continuous. See the implementation details below for more comments on this definition.
• WithSeminorms.continuousLinearMapOfTendsto: fix E a barrelled space and F a TVS satisfying WithSeminorms q for some q. Given a sequence of continuous linear maps from E to F that converges pointwise to a function f : E → F, this bundles f as a continuous linear map using the Banach-Steinhaus theorem.

## Main theorems #

• BaireSpace.instBarrelledSpace: any TVS that is also a BaireSpace is barrelled. In particular, this applies to Banach spaces and Fréchet spaces.
• WithSeminorms.banach_steinhaus: the Banach-Steinhaus theorem, also called Uniform Boundedness Principle. Fix E a barrelled space and F a TVS satisfying WithSeminorms q for some q. Any family 𝓕 : ι → E →L[𝕜] F of continuous linear maps that is pointwise bounded is (uniformly) equicontinuous. Here, pointwise bounded means that for all k and x, the family of real numbers i ↦ q k (𝓕 i x) is bounded above, which is equivalent to requiring that 𝓕 is pointwise Von Neumann bounded (see WithSeminorms.image_isVonNBounded_iff_seminorm_bounded).

## Implementation details #

Barrelled spaces are defined in Bourbaki as locally convex spaces where barrels (aka closed balanced absorbing convex sets) are neighborhoods of zero. One can then show that barrels in a locally convex space are exactly closed unit balls of lower semicontinuous seminorms, hence that a locally convex space is barrelled iff any lower semicontinuous seminorm is continuous.

The problem with this definition is the local convexity, which is essential to prove that the barrel definition is equivalent to the seminorm definition, because we can essentially only use LocallyConvexSpace over ℝ or ℂ (which is indeed the setup in which Bourbaki does most of the theory). Since we can easily prove the normed space version over any NontriviallyNormedField, this wouldn't make for a very satisfying "generalization".

Fortunately, it turns out that using the seminorm definition directly solves all problems, since it is exactly what we need for the proof. One could then expect to need the barrel characterization to prove that Baire TVS are barrelled, but the proof is actually easier to do with the seminorm characterization!

## TODO #

• define barrels and prove that a locally convex space is barrelled iff all barrels are neighborhoods of zero.
• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

## Tags #

banach-steinhaus, uniform boundedness, equicontinuity