46 Functional analysis

TheoremBanach–Alaoglu theorem#

The Banach-Alaoglu theorem: the polar set of a neighborhood s of the origin in a normed space E is a compact subset of WeakDual 𝕜 E.

WeakDual.isCompact_polar.{u_1, u_3} (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜]
  [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] {s : Set E} (s_nhds : s ∈ nhds 0) :
  IsCompact (WeakDual.polar 𝕜 s)
Sources
MathlibWeakDual.isCompact_polar
Uses 8
Statement usesAssociative algebra over a commutative ring · Compactness in terms of filters · Dual of a normed space · Normed vector space over a normed field · Topological ring
Proof usesClosure · Tychonoff's theorem · Weak-* topology for dualities

TheoremClosed graph theorem#

The closed graph theorem : a linear map between two Banach spaces whose graph is closed is continuous.

LinearMap.continuous_of_isClosed_graph.{u_1, u_3, u_5} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (g : E →ₗ[𝕜] F)
  (hg : IsClosed ↑g.graph) : Continuous ⇑g
Sources
MathlibLinearMap.continuous_of_isClosed_graph
Uses 6 · Used by 1
Statement usesCompleteness · Continuous function · Linear map · Normed vector space over a normed field · Product of vector spaces
Proof usesRange of a linear map
Used byHellinger–Toeplitz theorem

DefinitionGelfand–Mazur theorem#

Mathlib records this with 3 declarations.

NormedRing.algEquivComplexOfComplete: Gelfand-Mazur theorem: For a complex Banach division algebra, the natural algebraMap ℂ A is an algebra isomorphism whose inverse is given by selecting the (unique) element of spectrum ℂ a. In addition, algebraMap_isometry guarantees this map is an isometry.

Note: because NormedDivisionRing requires the field norm_mul : ∀ a b, ‖a * b‖ = ‖a‖ * ‖b‖, we don't use this type class and instead opt for a NormedRing in which the nonzero elements are precisely the units. This allows for the application of this isomorphism in broader contexts, e.g., to the quotient of a complex Banach algebra by a maximal ideal. In the case when A is actually a NormedDivisionRing, one may fill in the argument hA with the lemma isUnit_iff_ne_zero.

NormedRing.algEquivComplexOfComplete.{u_2} {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A]
  [CompleteSpace A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) : ℂ ≃ₐ[ℂ] A

NormedAlgebra.Complex.algEquivOfNormMul: A version of the Gelfand-Mazur Theorem.

If F is a nontrivial normed ℂ-algebra with multiplicative norm, then we obtain a ℂ-algebra equivalence with ℂ.

NormedAlgebra.Complex.algEquivOfNormMul.{u_1} (F : Type u_1) [NormedRing F] [NormOneClass F]
  [NormMulClass F] [NormedAlgebra ℂ F] [Nontrivial F] : ℂ ≃ₐ[ℂ] F

NormedAlgebra.Real.nonempty_algEquiv_or: A version of the Gelfand-Mazur Theorem over ℝ.

If a field F is a normed ℝ-algebra, then F is isomorphic as an ℝ-algebra either to ℝ or to ℂ.

NormedAlgebra.Real.nonempty_algEquiv_or.{u_2} (F : Type u_2) [NormedField F] [NormedAlgebra ℝ F] :
  Nonempty (F ≃ₐ[ℝ] ℝ) ∨ Nonempty (F ≃ₐ[ℝ] ℂ)

The first two are over the complex numbers (with different assumptions), the third is over the real numbers.

Sources
MathlibNormedRing.algEquivComplexOfComplete · NormedAlgebra.Complex.algEquivOfNormMul · NormedAlgebra.Real.nonempty_algEquiv_or
Uses 8
Statement usesAssociative algebra over a commutative ring · Completeness · Complex number · Metric space
Proof usesAlgebraic extension · Connectedness · Fundamental theorem of algebra · The Triangle Inequality

TheoremHellinger–Toeplitz theorem#

The Hellinger--Toeplitz theorem: if a symmetric operator is defined on a complete space, then it is automatically continuous.

LinearMap.IsSymmetric.continuous.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →ₗ[𝕜] E}
  (hT : T.IsSymmetric) : Continuous ⇑T
Sources
MathlibLinearMap.IsSymmetric.continuous
Uses 6 · Used by 1
Statement usesContinuous function · Inner product space, over \(R\) or \(C\) · Linear map
Proof usesClosed graph theorem · Hausdorff space · Ordered ring
Used byEigenvalues from Rayleigh quotient

TheoremM. Riesz extension theorem#

M. Riesz extension theorem: given a convex cone s in a vector space E, a submodule p, and a linear f : p → ℝ, assume that f is nonnegative on p ∩ s and p + s = E. Then there exists a globally defined linear function g : E → ℝ that agrees with f on p, and is nonnegative on s.

riesz_extension.{u_1} {E : Type u_1} [AddCommGroup E] [_root_.Module ℝ E] (s : PointedCone ℝ E)
  (f : E →ₗ.[ℝ] ℝ) (nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x)
  (dense : ∀ (y : E), ∃ x, ↑x + y ∈ s) : ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ x ∈ s, 0 ≤ g x
Sources
Mathlibriesz_extension
Uses 7
Statement usesLinear map · Pointed cone · Real number
Proof usesField \(\R\) of real numbers · Generating sets · Order · Sum of subspaces

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.