Thm. 3.0.1 — Banach–Steinhaus for Fréchet and LF-spaces

Proved

GarrettFA.banach_steinhaus

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysistopological-vector-spaces

Let $X$ be a Fréchet space or an LF-space and $Y$ a locally convex topological vector space over $\mathbb K=\mathbb R$ or $\mathbb C$ . Let $E$ be a set of continuous linear maps $X\to Y$ such that for every $x\in X$ the orbit

E x=\{\,Tx : T\in E\,\}

is bounded in $Y$ . Then $E$ is equicontinuous.

This uniform boundedness principle is what makes pointwise limits of operators continuous in Theorem 4.1.1.

Formalization Note The notes say "a set $E$ of linear maps". The statement is false for discontinuous maps: a single discontinuous linear functional on a Banach space has bounded orbits but is not equicontinuous. The proof in the notes uses closedness of $T^{-1}U$ , so continuity of the maps is assumed here.

Preamble

import Definitions.Def_GarrettFA_IsEquicontinuousSet
import Definitions.Def_GarrettFA_IsFrechetSpace
import Definitions.Def_GarrettFA_IsLFSpace

Formal statement

namespace GarrettFA
theorem banach_steinhaus {𝕜 : Type*} [RCLike 𝕜] {X : Type*} [AddCommGroup X] [Module 𝕜 X] [Module ℝ X]
    [IsScalarTower ℝ 𝕜 X] [UniformSpace X] [IsUniformAddGroup X] [ContinuousSMul 𝕜 X] [T2Space X]
    (hX : IsFrechetSpace 𝕜 X ∨ IsLFSpace 𝕜 X)
    {Y : Type*} [AddCommGroup Y] [Module 𝕜 Y] [Module ℝ Y] [IsScalarTower ℝ 𝕜 Y]
    [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul 𝕜 Y] [LocallyConvexSpace ℝ Y]
    [T2Space Y]
    (E : Set (X →L[𝕜] Y))
    (hE : ∀ x : X, Bornology.IsVonNBounded 𝕜 ((fun T : X →L[𝕜] Y => T x) '' E)) :
    IsEquicontinuousSet ((fun T : X →L[𝕜] Y => (T : X → Y)) '' E) := by sorry
end GarrettFA

Source

Paul Garrett, *Completeness and quasi-completeness* (lecture notes, April 24, 2014), http://www.math.umn.edu/~garrett/m/fun/notes_2012-13/07d_quasi-completeness.pdf, p. 4, Theorem 3.0.1 (with continuity of the maps, which the proof uses)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $\mathbb K$ be a real-or-complex scalar field (in practice $\mathbb R$ or $\mathbb C$ ). Let $X$ be a $\mathbb K$ -vector space that is also a real vector space with compatible scalar multiplications, carrying a uniform structure for which addition and subtraction are uniformly continuous (so the uniformity is the canonical translation-invariant uniformity of the induced topology), with scalar multiplication $\mathbb K\times X\to X$ jointly continuous, and Hausdorff, and assume that $X$ is Fréchet or $X$ is an LF-space. Fréchet (the bundle's definition, applied to the given uniform structure): locally convex as a real topological vector space, the topology is metrizable, and the space is complete for its uniform structure (every Cauchy filter converges). LF-space (the bundle's definition): there exists a sequence of $\mathbb K$ -subspaces $F_0,F_1,\dots$ of the space such that the space is the strict colimit of $(F_n)$ in the sense above, and for every $n$ the subspace $F_n$ , with the subspace topology, is metrizable, and $F_n$ is a complete subset for the ambient uniform structure.

Let $Y$ be a $\mathbb K$ -vector space that is also a real vector space with compatible scalar multiplications (multiplying by a real number $r$ is the same as multiplying by $r\in\mathbb K$ ), carrying a topology in which addition and negation are continuous, scalar multiplication $\mathbb K\times Y\to Y$ is jointly continuous, and which is Hausdorff, which is moreover locally convex as a real topological vector space. Let $E$ be a set of continuous $\mathbb K$ -linear maps $X\to Y$ such that for every $x\in X$ the set $\{Tx : T\in E\}$ is bounded in $Y$ . Here bounded means von Neumann bounded over $\mathbb K$ : every neighbourhood of $0$ absorbs the set (for each neighbourhood $U$ of $0$ there is $r>0$ such that the set is contained in $cU$ for all scalars $c\in\mathbb K$ with $|c|\ge r$ ).

Then $E$ (as a set of functions $X\to Y$ ) is equicontinuous. Equicontinuous (the bundle's definition): for every neighbourhood $U$ of $0$ in the target there is a neighbourhood $N$ of $0$ in the source with $T(N)\subseteq U$ for every map $T$ in the family.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph