Functional analysis

Content created by Louis Wasserman.

Created on 2025-12-27.
Last modified on 2025-12-27.

module functional-analysis where

open import functional-analysis.absolute-convergence-series-real-banach-spaces public
open import functional-analysis.additive-complete-metric-abelian-groups-real-banach-spaces public
open import functional-analysis.convergent-series-real-banach-spaces public
open import functional-analysis.real-banach-spaces public
open import functional-analysis.real-hilbert-spaces public
open import functional-analysis.series-real-banach-spaces public
open import functional-analysis.sums-of-finite-sequences-of-elements-real-banach-spaces public

External links

• Functional analysis on Wikipedia

Recent changes

• 2025-12-27. Louis Wasserman. Split out functional analysis as its own module (#1766).