# 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
`Mathlib.Analysis.Normed.Operator.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.

## References #

## Tags #

banach-steinhaus, uniform boundedness, equicontinuity

A topological vector space `E`

is said to be **barrelled** if all lower semicontinuous
seminorms on `E`

are actually continuous. This is not the usual definition for TVS over `β`

or `β`

,
but this has the big advantage of working and giving sensible results over *any*
`NontriviallyNormedField`

. In particular, the Banach-Steinhaus theorem holds for maps between such
a space and any space whose topology is generated by a family of seminorms.

- continuous_of_lowerSemicontinuous : β (p : Seminorm π E), LowerSemicontinuous βp β Continuous βp
In a barrelled space, all lower semicontinuous seminorms on

`E`

are actually continuous.

## Instances

In a barrelled space, all lower semicontinuous seminorms on `E`

are actually continuous.

Any TVS over a `NontriviallyNormedField`

that is also a Baire space is barrelled. In
particular, this applies to Banach spaces and FrΓ©chet spaces.

## Equations

- β― = β―

The **Banach-Steinhaus** theorem, or **Uniform Boundedness Principle**, for maps from a
barrelled space to any space whose topology is generated by a family of seminorms. Use
`WithSeminorms.equicontinuous_TFAE`

and `Seminorm.bound_of_continuous`

to get explicit bounds on
the seminorms from equicontinuity.

Given a sequence of continuous linear maps which converges pointwise and for which the
domain is barrelled, the Banach-Steinhaus theorem is used to guarantee that the limit map
is a *continuous* linear map as well.

This actually works for any *countably generated* filter instead of `atTop : Filter β`

,
but the proof ultimately goes back to sequences.

## Equations

- hq.continuousLinearMapOfTendsto g h = { toLinearMap := linearMapOfTendsto f (fun (a : Ξ±) => β(g a)) h, cont := β― }