Documentation

Mathlib.Analysis.Normed.Operator.BanachSteinhaus

The Banach-Steinhaus theorem: Uniform Boundedness Principle #

Herein we prove the Banach-Steinhaus theorem for normed spaces: any collection of bounded linear maps from a Banach space into a normed space which is pointwise bounded is uniformly bounded.

Note that we prove the more general version about barrelled spaces in Analysis.LocallyConvex.Barrelled, and the usual version below is indeed deduced from the more general setup.

theorem banach_steinhaus {E : Type u_1} {F : Type u_2} {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] {ฮน : Type u_5} [CompleteSpace E] {g : ฮน โ†’ E โ†’SL[ฯƒโ‚โ‚‚] F} (h : โˆ€ (x : E), โˆƒ (C : โ„), โˆ€ (i : ฮน), โ€–(g i) xโ€– โ‰ค C) :
โˆƒ (C' : โ„), โˆ€ (i : ฮน), โ€–g iโ€– โ‰ค C'

This is the standard Banach-Steinhaus theorem, or Uniform Boundedness Principle. If a family of continuous linear maps from a Banach space into a normed space is pointwise bounded, then the norms of these linear maps are uniformly bounded.

See also WithSeminorms.banach_steinhaus for the general statement in barrelled spaces.

theorem banach_steinhaus_iSup_nnnorm {E : Type u_1} {F : Type u_2} {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] {ฮน : Type u_5} [CompleteSpace E] {g : ฮน โ†’ E โ†’SL[ฯƒโ‚โ‚‚] F} (h : โˆ€ (x : E), โจ† (i : ฮน), โ†‘โ€–(g i) xโ€–โ‚Š < โŠค) :
โจ† (i : ฮน), โ†‘โ€–g iโ€–โ‚Š < โŠค

This version of Banach-Steinhaus is stated in terms of suprema of โ†‘โ€–ยทโ€–โ‚Š : โ„โ‰ฅ0โˆž for convenience.

@[reducible, inline]
abbrev continuousLinearMapOfTendsto {E : Type u_1} {F : Type u_2} {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField ๐•œ] [NontriviallyNormedField ๐•œโ‚‚] [NormedSpace ๐•œ E] [NormedSpace ๐•œโ‚‚ F] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] {ฮฑ : Type u_5} [CompleteSpace E] [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 complete, the Banach-Steinhaus theorem is used to guarantee that the limit map is a continuous linear map as well.

Equations
Instances For