02.11.04 · analysis / functional-analysis

Banach space fundamentals

shipped3 tiersLean: partial

Anchor (Master): Reed-Simon Vol. I §III; Conway §III

Intuition [Beginner]

A vector space lets you add vectors and stretch them. A norm adds a way to measure size. A Banach space adds one more promise: if a list of vectors settles down so tightly that its later terms become indistinguishable, then it actually settles on a vector inside the space.

That last promise is called completeness. It rules out missing limit points.

The rational numbers are not complete as a line: decimal approximations to get closer and closer to each other, but their target is not rational. The real numbers repair that hole. Banach spaces are the same repair for spaces of functions, sequences, and solutions to equations.

Visual [Beginner]

The left space contains the endpoint of every Cauchy path. The right space has a hole, so a path can settle toward a point that is not present.

Cauchy sequence landing inside a complete space and approaching a missing point in an incomplete space.

Completeness is not about drawing every possible curve. It is about whether the space contains the limits that its own distance measurement forces.

Worked example [Beginner]

Take the space of continuous functions on the interval from to . Measure a function by its largest absolute height:

If a list of continuous functions gets uniformly closer and closer, then it has a uniform limit. That limit is still continuous. So this function space is Banach.

Now take only polynomial functions with the same measurement. A list of polynomials can settle toward on the interval from to . The target is continuous but not a polynomial. The polynomial space has a missing limit, so it is not complete.

Check your understanding [Beginner]

Formal definition [Intermediate+]

Let be a vector space over or 01.01.03. A norm on is a function such that:

  1. iff ;
  2. for every scalar ;
  3. .

The norm defines a metric . A sequence is Cauchy if, for every , there is such that implies .

A Banach space is a normed vector space in which every Cauchy sequence converges to an element of the same space [Conway §III].

Standard examples include , , the sequence spaces for , and with the supremum norm when is compact. The space of polynomials with the supremum norm on a compact interval is not Banach: its completion is the closure of the polynomials inside .

Key theorem with proof [Intermediate+]

Theorem (closed subspaces of Banach spaces are Banach). Let be a Banach space and let be a linear subspace with the restricted norm. Then is Banach if and only if is closed in .

Proof. First assume is closed. Let be a Cauchy sequence in . It is also Cauchy in , so completeness of gives a limit with . Since is closed and every lies in , the limit lies in . Thus every Cauchy sequence in converges in .

Conversely, assume is Banach. Let be a sequence in converging in to some . Every convergent sequence is Cauchy, so is Cauchy in . Completeness of gives such that in the restricted norm. Limits in a metric space are unique, so . Hence , and is closed.

Bridge. The construction here builds toward 02.11.01 (bounded linear operators), where the same data is upgraded, and the symmetry side is taken up in 02.11.05 (compact operators). The defining pattern appears again in those units in a sharpened form, where the local data is glued or quotiented. Putting these together, the foundational insight is that the data of this unit gives the structural signature that the rest of the strand reads off.

Exercises [Intermediate+]

Lean formalization [Intermediate+]

lean_status: partial — Mathlib models Banach spaces with existing normed-space typeclasses plus CompleteSpace. The companion module records the intended predicate name; the deeper theorems used downstream, such as Fredholm theory and compact-operator quotients, remain outside this unit.

[object Promise]

Fundamental theorems [Master]

Three theorems make Banach spaces the natural domain for functional analysis. The Baire category theorem implies that a complete metric space cannot be written as a countable union of nowhere dense closed sets. From it follow the uniform boundedness principle, the open mapping theorem, and the closed graph theorem [Reed-Simon Vol. I §III].

The open mapping theorem says that a surjective bounded linear map between Banach spaces sends open sets to open sets. Equivalently, a bijective bounded linear map between Banach spaces has a bounded inverse. The closed graph theorem says that a linear map between Banach spaces is bounded exactly when its graph is closed in the product Banach space.

These results fail in useful forms without completeness. Completeness is not a decorative hypothesis; it is the engine that turns pointwise or algebraic control into norm control.

Completions and examples [Master]

Every normed vector space has a completion , together with an isometric linear map whose image is dense. The completion is unique up to unique isometric isomorphism. This universal property lets one build Banach spaces from dense algebraic subspaces without changing the intended limiting theory.

Important completions include spaces from simple functions, spaces from finite-support sequences, and Sobolev spaces from smooth functions under weak-derivative norms. Differential equations and elliptic operators use these completions because estimates naturally control norms rather than pointwise formulas [quantum-well Analysis (index).md].

The Fredholm unit 03.09.06 assumes Banach spaces because kernels, ranges, cokernels, and inverse-modulo-compact arguments require the closed-subspace and bounded-inverse machinery.

Connections [Master]

  • Vector space 01.01.03 — Banach spaces add norms and completeness to vector spaces.

  • Hilbert space 02.11.08 — Hilbert spaces are Banach spaces whose norm comes from an inner product.

  • Bounded linear operators 02.11.01 — operator norms and continuity are formulated between Banach spaces.

  • Compact operators 02.11.05 — compactness in infinite-dimensional Banach spaces controls Fredholm perturbations.

  • Fredholm operators 03.09.06 — Fredholm theory is a Banach-space theory before it becomes an elliptic-operator theory.

Historical & philosophical context [Master]

Banach's 1932 monograph placed complete normed linear spaces at the center of analysis, unifying sequence spaces, function spaces, and linear operators. The name "Banach space" reflects that synthesis rather than a single example.

The early twentieth-century shift from formulas to spaces changed the status of existence theorems. Completeness allowed analysts to construct solutions as limits of approximations, while bounded linear maps became the stable morphisms of the category [Conway §III].

Bibliography [Master]

  • Banach, S., Theorie des operations lineaires, Warsaw, 1932.
  • Reed, M. and Simon, B., Methods of Modern Mathematical Physics, Vol. I: Functional Analysis, Academic Press, 1980. §III.
  • Conway, J. B., A Course in Functional Analysis, 2nd ed., Springer, 1990. §III.
  • Yosida, K., Functional Analysis, Springer, 1980.

Wave 2 Phase 2.2 unit #3. Produced as the Banach-space prerequisite for Fredholm operators and later bounded/compact operator units.