mathlib documentation

analysis.normed_space.banach_steinhaus

The Banach-Steinhaus theorem: Uniform Boundedness Principle #

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

TODO #

For now, we only prove the standard version by appeal to the Baire category theorem. Much more general versions exist (in particular, for maps from barrelled spaces to locally convex spaces), but these are not yet in mathlib.

source
theorem banach_steinhaus {E : Type u_1} {F : Type u_2} {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] [nontrivially_normed_field π•œ] [nontrivially_normed_field π•œβ‚‚] [normed_space π•œ E] [normed_space π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] {ΞΉ : Type u_5} [complete_space 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.

source
theorem banach_steinhaus_supr_nnnorm {E : Type u_1} {F : Type u_2} {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] [nontrivially_normed_field π•œ] [nontrivially_normed_field π•œβ‚‚] [normed_space π•œ E] [normed_space π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] {ΞΉ : Type u_5} [complete_space 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.

source
def continuous_linear_map_of_tendsto {E : Type u_1} {F : Type u_2} {π•œ : Type u_3} {π•œβ‚‚ : Type u_4} [seminormed_add_comm_group E] [seminormed_add_comm_group F] [nontrivially_normed_field π•œ] [nontrivially_normed_field π•œβ‚‚] [normed_space π•œ E] [normed_space π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [ring_hom_isometric σ₁₂] [complete_space E] [t2_space F] (g : β„• β†’ (E β†’SL[σ₁₂] F)) {f : E β†’ F} (h : filter.tendsto (Ξ» (n : β„•) (x : E), ⇑(g n) x) filter.at_top (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