22.3. Banach and Hilbert spaces
To add a Banach space to the environment one writes:
variable (E 𝕜 : Type*) [NormedField 𝕜]
[NormedAddCommGroup E] [NormedSpace 𝕜 E]
[CompleteSpace E]
Special notation for the norm is available for vectors in a Banach space:
example (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ := norm_add_le x y
For a Hilbert space one writes:
variable (E 𝕜 : Type*) [RCLike 𝕜]
[NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
[CompleteSpace E]
Special notation for the inner product is available for vectors in a Hilbert
space after opening the InnerProductSpace scope:
open scoped InnerProductSpace
example (x y : E) :
⟪x + y, x + y⟫_𝕜 + ⟪x - y, x - y⟫_𝕜 =
2 * (⟪x, x⟫_𝕜 + ⟪y, y⟫_𝕜) :=
parallelogram_law
22.3.1. Notable results
The following are some notable results in Mathlib's theory library of topological vector spaces:
-
The open mapping theorem:
ContinuousLinearMap.isOpenMap -
The Hahn-Banach theorem:
exists_extension_norm_eq -
The Lax-Milgram theorem:
IsCoercive.continuousLinearEquivOfBilin -
The Banach-Steinhaus theorem:
banach_steinhaus -
The Riesz representation theorem:
InnerProductSpace.toDual -
The Banach-Alaoglu theorem:
WeakDual.isCompact_polar