English
Let E be a barrelled space and F a topological vector space whose topology is generated by a family of seminorms q on F. If (T_i) is a family of continuous linear maps from E to F such that for every k and every x, the set {q_k(T_i x) : i} is bounded, then the family {T_i} is uniformly equicontinuous; i.e., for every neighborhood W of 0 in F there exists a neighborhood U of 0 in E with T_i(U) ⊆ W for all i.
Русский
Пусть E — барельевское пространство, F — т.д. топологическое векторное пространство порождаемое семинормами q. Пусть (T_i) — семейство непрерывных линейных отображений E → F. Если для каждого k и каждого x выполняется, что множество {q_k(T_i x)} ограничено сверху по i, тогда семейство {T_i} является равномерно равнобесконечным в смысле непрерывности: для любой окрестности W 0 в F существует окрестность U 0 в E такая, что T_i(U) ⊆ W для всех i.
LaTeX
$$$\displaystyle \text{If }E\text{ is barrelled and }F\text{ has a topology generated by a family }q=(q_k)_{k\in\kappa},\; (T_i)_{i\in I}\subseteq \mathcal{L}(E,F) \text{ with } T_i\text{ continuous, and }\forall k,\forall x:\; \sup_{i\in I} q_k(T_i x)<\infty, \\ \text{then } \{T_i\}_{i\in I} \text{ is uniformly equicontinuous, i.e. } \forall W\ni 0_F\;\exists U\ni 0_E:\ \forall i:\; T_i(U)\subseteq W.$$$$
Lean4
/-- 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. -/
protected theorem banach_steinhaus (H : ∀ k x, BddAbove (range fun i ↦ q k (𝓕 i x))) :
UniformEquicontinuous ((↑) ∘ 𝓕) := by
-- We just have to prove that `⊔ i, (q k) ∘ (𝓕 i)` is a (well-defined) continuous seminorm
-- for all `k`.
refine (hq.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup (toLinearMap ∘ 𝓕)).mpr ?_
intro k
have : BddAbove (range fun i ↦ (q k).comp (𝓕 i).toLinearMap) :=
by
rw [Seminorm.bddAbove_range_iff]
exact H k
exact ⟨this, Seminorm.continuous_iSup _ (fun i ↦ (hq.continuous_seminorm k).comp (𝓕 i).continuous) this⟩
