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 spaceE
is said to be barrelled if all lower semicontinuous seminorms onE
are actually continuous. See the implementation details below for more comments on this definition.WithSeminorms.continuousLinearMapOfTendsto
: fixE
a barrelled space andF
a TVS satisfyingWithSeminorms q
for someq
. Given a sequence of continuous linear maps fromE
toF
that converges pointwise to a functionf : E β F
, this bundlesf
as a continuous linear map using the Banach-Steinhaus theorem.
Main theorems #
BaireSpace.instBarrelledSpace
: any TVS that is also aBaireSpace
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. FixE
a barrelled space andF
a TVS satisfyingWithSeminorms q
for someq
. Any familyπ : ΞΉ β E βL[π] F
of continuous linear maps that is pointwise bounded is (uniformly) equicontinuous. Here, pointwise bounded means that for allk
andx
, the family of real numbersi β¦ q k (π i x)
is bounded above, which is equivalent to requiring thatπ
is pointwise Von Neumann bounded (seeWithSeminorms.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
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 := β― }