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

• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

Tags

banach-steinhaus, uniform boundedness, equicontinuity

class BarrelledSpace (𝕜 : Type u_1) (E : Type u_2) [SeminormedRing 𝕜] [AddGroup E] [SMul 𝕜 E] [TopologicalSpace E] : Prop

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.

theorem BarrelledSpace.continuous_of_lowerSemicontinuous {𝕜 : Type u_1} {E : Type u_2} : ∀ {inst : SeminormedRing 𝕜} {inst_1 : AddGroup E} {inst_2 : SMul 𝕜 E} {inst_3 : TopologicalSpace E} [self : BarrelledSpace 𝕜 E] (p : Seminorm 𝕜 E), LowerSemicontinuous ⇑p → Continuous ⇑p

In a barrelled space, all lower semicontinuous seminorms on E are actually continuous.

theorem Seminorm.continuous_of_lowerSemicontinuous {𝕜 : Type u_1} {E : Type u_2} [AddGroup E] [SMul 𝕜 E] [SeminormedRing 𝕜] [TopologicalSpace E] [BarrelledSpace 𝕜 E] (p : Seminorm 𝕜 E) (hp : LowerSemicontinuous ⇑p) : Continuous ⇑p

theorem Seminorm.continuous_iSup {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [BarrelledSpace 𝕜 E] (p : ι → Seminorm 𝕜 E) (hp : ∀ (i : ι), Continuous ⇑(p i)) (bdd : BddAbove (Set.range p)) : Continuous (⨆ (i : ι), ⇑(p i))

instance BaireSpace.instBarrelledSpace {𝕜₁ : Type u_4} {E : Type u_6} [NontriviallyNormedField 𝕜₁] [AddCommGroup E] [Module 𝕜₁ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜₁ E] [BaireSpace E] : BarrelledSpace 𝕜₁ E

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

• ⋯ = ⋯

theorem WithSeminorms.banach_steinhaus {ι : Type u_2} {κ : Type u_3} {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} {E : Type u_6} {F : Type u_7} [Nonempty κ] [NontriviallyNormedField 𝕜₁] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [UniformSpace E] [UniformSpace F] [UniformAddGroup E] [UniformAddGroup F] [ContinuousSMul 𝕜₁ E] [BarrelledSpace 𝕜₁ E] {𝓕 : ι → E →SL[σ₁₂] F} {q : SeminormFamily 𝕜₂ F κ} (hq : WithSeminorms q) (H : ∀ (k : κ) (x : E), BddAbove (Set.range fun (i : ι) => (q k) ((𝓕 i) x))) : UniformEquicontinuous (DFunLike.coe ∘ 𝓕)

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.

def WithSeminorms.continuousLinearMapOfTendsto {α : Type u_1} {κ : Type u_3} {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} {E : Type u_6} {F : Type u_7} [Nonempty κ] [NontriviallyNormedField 𝕜₁] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂} [RingHomIsometric σ₁₂] [AddCommGroup E] [AddCommGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [UniformSpace E] [UniformSpace F] [UniformAddGroup E] [UniformAddGroup F] [ContinuousSMul 𝕜₁ E] [BarrelledSpace 𝕜₁ E] {q : SeminormFamily 𝕜₂ F κ} [ContinuousSMul 𝕜₂ F] (hq : WithSeminorms q) [T2Space F] {l : Filter α} [l.IsCountablyGenerated] [l.NeBot] (g : α → E →SL[σ₁₂] F) {f : E → F} (h : Filter.Tendsto (fun (n : α) (x : E) => (g n) x) l (nhds f)) : E →SL[σ₁₂] F

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 := ⋯ }