Mathlib Map

Map · 46

functional analysis

MSC 46 · Functional analysis

14,935 declarations (11,773 theorems, 3,162 definitions) across 346 files. 12 of the 58 famous theorems listed for this area are in Mathlib (21%), 13 in some Lean library. 9 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas12

  • 46B Normed linear spaces and Banach spaces; Banach lattices 4,583
  • 46A Topological linear spaces and related structures 3,085
  • 46L Selfadjoint operator algebras (\(C^*\)-algebras, von Neumann (\(W^*\)-) algebras, etc.) 2,203
  • 46C Inner product spaces and their generalizations, Hilbert spaces 1,552
  • 46H Topological algebras, normed rings and algebras, Banach algebras 1,305
  • 46E Linear function spaces and their duals 1,023
  • 46F Distributions, generalized functions, distribution spaces 845
  • 46G Measures, integration, derivative, holomorphy (all involving infinite-dimensional spaces) 169
  • 46T Nonlinear functional analysis 65
  • 46M Methods of category theory in functional analysis 62
  • 46K Topological (rings and) algebras with an involution 27
  • 46S Other (nonclassical) types of functional analysis 16

Famous theorems12 of 58

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 46

In Mathlib · 12

From the 100 theorems list2

Open conjectures stated in Lean9

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing25 of 39

From Mathlib's own undergraduate checklist.

Distribution calculus · 25 of 39

  • Spaces $\mathcal{D}(\R^d)$ › stability by derivation
  • Spaces $\mathcal{D}(\R^d)$ › stability by multiplication by a smooth function
  • Spaces $\mathcal{D}(\R^d)$ › partitions of unity
  • Spaces $\mathcal{D}(\R^d)$ › constructing approximations of probability density functions in spaces of common functions (trig, exp, rational, log, etc)
  • Distributions on $\R^d$ › locally integrable functions as distributions
  • Distributions on $\R^d$ › derivative of a distribution
  • Distributions on $\R^d$ › Dirac measures
  • Distributions on $\R^d$ › derivatives of Dirac measures
  • Distributions on $\R^d$ › derivative of the Heaviside function
  • Distributions on $\R^d$ › Cauchy principal values
  • Distributions on $\R^d$ › multiplication by a smooth function
  • Distributions on $\R^d$ › convergence of sequences of distributions
  • Distributions on $\R^d$ › support of a distribution
  • Spaces $\mathcal{S}(\R^d)$ › Gaussian functions
  • Tempered distributions › $L^2$ functions and Riesz representation
  • Tempered distributions › periodic functions
  • Tempered distributions › Dirac comb
  • Tempered distributions › Fourier transform and derivation
  • Tempered distributions › Fourier transform and convolution product
  • Applications › using convolution and Fourier-Laplace transform to solve one-dimensional linear differential equations
  • Applications › weak solution of partial derivative equation
  • Applications › fundamental solution of the Laplacian
  • Applications › solving the Laplace equations
  • Applications › heat equations
  • Applications › wave equations

Structures defined here24

Typeclasses defined in this area's files, most assumed first.

Files346

Largest first. The code after each file is its assigned subarea.