Normed vector spaces/Banach spaces

ClassNormed vector space over a normed field#

A normed space over a normed field is a vector space endowed with a norm which satisfies the equality ‖c • x‖ = ‖c‖ ‖x‖. We require only ‖c • x‖ ≤ ‖c‖ ‖x‖ in the definition, then prove ‖c • x‖ = ‖c‖ ‖x‖ in norm_smul.

Note that since this requires SeminormedAddCommGroup and not NormedAddCommGroup, this typeclass can be used for "seminormed spaces" too, just as Module can be used for "semimodules".

NormedSpace.{u_6, u_7} (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] :
  Type (max u_6 u_7)
Sources
MathlibNormedSpace
Uses 2 · Used by 65
Statement usesMetric space · Module
Used byLiouville’s Theorem and the Construction of Transcendental Numbers · Minkowski’s Fundamental Theorem · L’Hopital’s Rule · The Mean Value Theorem (Freek Wiedijk's 100 theorems) · Theorem of Ceva · Liouville theorem · Maximum modulus principle · Removable singularity · Schwarz lemma · Derivative of a composition of functions (Analysis) · Derivative of the inverse of a function (Analysis) · Implicit function theorem · Inverse function theorem (Differentiability) · Leibniz formula (Analysis) · Local extrema · Mean value theorem (Differentiability) · Inner product space, over \(R\) or \(C\) · Bochner integral · Banach open mapping theorem · Banach-Steinhaus theorem · Hahn-Banach theorem · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Isometric inclusion in double dual · Boundary of a manifold · Integral curves · Interior of a manifold · Lie algebra of a Lie group · Pullback of vector fields · Tangent bundle · Covariant derivatives · Topological vector bundle · Urysohn's lemma · Abel's theorem · Darboux's theorem (analysis) · Fermat's theorem (stationary points) · Rademacher's theorem · Euler's theorem on homogeneous functions · Banach–Alaoglu theorem · Closed graph theorem · Akra–Bazzi theorem · Hahn embedding theorem · Niven's theorem · Poisson limit theorem · Cocyclicity · Isometries of a Euclidean affine space · Chain rule · Directional derivative · Inverse function theorem (Differential calculus) · Partial derivatives commute · Cauchy-Lipschitz Theorem · Grönwall lemma · Radius of convergence · Holomorphic stability under uniform convergence · Continuity (continuity and differentiability of convex functions) · Derivative of a composition of functions (Single Variable Real Analysis) · Derivative of the inverse of a function (Single Variable Real Analysis) · Higher-order derivatives of functions · Leibniz formula (Single Variable Real Analysis) · Riemann sums · Alternating series · Differentiability of the limit of a sequence of functions · Differentiability of the sum of a series of functions · Weierstrass polynomial approximation theorem · Normed space of bounded continuous functions · Norms \(\lVert\cdot\rVert_p\) on \(\R^n\) and \(\C^n\)

TheoremTopology on a normed vector space#

Mathlib states this as NormSMulClass.toIsBoundedSMul.

NormSMulClass.toIsBoundedSMul.{u_1, u_2} {α : Type u_1} {β : Type u_2} [SeminormedRing α]
  [SeminormedAddCommGroup β] [_root_.Module α β] [NormSMulClass α β] : IsBoundedSMul α β
Sources
MathlibNormSMulClass.toIsBoundedSMul
Uses 3 · Used by 17
Statement usesBornology · Module · Order
Used byLeibniz formula (Analysis) · Existence of Hilbert basis · Regularization by convolution · Banach-Steinhaus theorem · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Sphere · Mean of product of independent random variables · Monotone convergence theorem (1000+ theorems) · Cauchy–Hadamard theorem · Euler's theorem on homogeneous functions · Partial derivatives commute · Taylor's theorem with integral form for remainder (Differential calculus) · Continuity (Complex-valued series) · Differentiability with respect to the complex variable · Alternating series · Differentiability of the limit of a sequence of functions · Taylor's theorem with Lagrange form for remainder

DefinitionEquivalence of norms in finite dimension#

The continuous linear equivalence induced by a linear equivalence on a finite-dimensional space.

LinearEquiv.toContinuousLinearEquiv.{u, v, w} {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜]
  {E : Type v} [AddCommGroup E] [_root_.Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F] [_root_.Module 𝕜 F] [TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [CompleteSpace 𝕜] [T2Space E] [T2Space F]
  [FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : E ≃L[𝕜] F
Sources
MathlibLinearEquiv.toContinuousLinearEquiv
Uses 6 · Used by 2
Statement usesCompleteness · Finite-dimensionality · Hausdorff space · Linear map · Metric space · Topological module
Used byHeine-Borel theorem (finite-dimensional normed spaces are proper) · Whitney embedding theorem

TheoremFinite-dimensional normed spaces over complete normed fields are complete#

A finite-dimensional subspace is complete.

Submodule.isComplete_of_finiteDimensional.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [UniformSpace E] [T2Space E]
  [IsUniformAddGroup E] [_root_.Module 𝕜 E] [ContinuousSMul 𝕜 E] (s : Submodule 𝕜 E)
  [FiniteDimensional 𝕜 ↥s] : IsComplete ↑s
Sources
MathlibSubmodule.isComplete_of_finiteDimensional
Uses 16
Statement usesCompleteness · Finite-dimensionality · Hausdorff space · Metric space · Topological module
Proof usesAffine space · Cardinal · Closure · Existence of bases · Field \(\R\) of real numbers · Induced topology · Isomorphism with \(K^n\) · Kernel of a linear map · Local ring · Quotient space (Fundamentals) · Topological ring

TheoremHeine-Borel theorem (finite-dimensional normed spaces are proper)#

Any finite-dimensional vector space over a locally compact field is proper. We do not register this as an instance to avoid an instance loop when trying to prove the properness of 𝕜, and the search for 𝕜 as an unknown metavariable. Declare the instance explicitly when needed.

FiniteDimensional.proper.{u, v} (𝕜 : Type u) [NontriviallyNormedField 𝕜] (E : Type v)
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [LocallyCompactSpace 𝕜] [FiniteDimensional 𝕜 E] :
  ProperSpace E
Sources
MathlibFiniteDimensional.proper
Uses 14 · Used by 9
Statement usesCompactness in terms of filters · Finite-dimensionality · Normed vector space over a normed field
Proof usesBasis · Cardinal · Continuous linear map · Equivalence of norms in finite dimension · Field \(\R\) of real numbers · Heine-Borel theorem (proper metric space version) · Linear independence · Local ring · Ordered ring · Topological ring · Topology on a normed vector space
Used byFourier Series · Riemann-Lebesgue lemma (Analysis) · Approximation by convolution · Change of variables formula · Rademacher's theorem · Fourier theorem · Lévy continuity theorem · Decomposition of an orthogonal transformation as a product of reflections · Log

DefinitionNorm of a continuous linear map#

Construct a continuous linear map from a linear map and a bound on this linear map. The fact that the norm of the continuous linear map is then controlled is given in LinearMap.mkContinuous_norm_le.

LinearMap.mkContinuous.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3}
  {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F]
  [_root_.Module 𝕜 E] [_root_.Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ℝ)
  (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : E →SL[σ] F
Sources
MathlibLinearMap.mkContinuous
Uses 3 · Used by 11
Statement usesBornology · Continuous linear map · Order
Used byPrinciple of isolated zeros · \(C^k\) function · Bochner integral · Smooth immersion · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners) · (smooth) vector bundle · Conditional expectation · Differentiability with respect to the complex variable · Taylor's theorem with Lagrange form for remainder · Example, the Hilbert basis of trigonometric polynomials

TheoremBanach-Steinhaus theorem#

This is the standard Banach-Steinhaus theorem, or Uniform Boundedness Principle. If a family of continuous linear maps from a Banach space into a normed space is pointwise bounded, then the norms of these linear maps are uniformly bounded.

See also WithSeminorms.banach_steinhaus for the general statement in barrelled spaces.

banach_steinhaus.{u_1, u_2, u_3, u_4, u_5} {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3}
  {𝕜₂ : Type u_4} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField 𝕜]
  [NontriviallyNormedField 𝕜₂] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂}
  [RingHomIsometric σ₁₂] {ι : Type u_5} [CompleteSpace E] {g : ι → E →SL[σ₁₂] F}
  (h : ∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C) : ∃ C', ∀ (i : ι), ‖g i‖ ≤ C'
Sources
Mathlibbanach_steinhaus
Uses 7
Statement usesCompleteness · Continuous linear map · Normed vector space over a normed field
Proof usesBaire theorem · The Triangle Inequality · Topological module · Topology on a normed vector space

TheoremBanach open mapping theorem#

The Banach open mapping theorem: a surjective bounded linear map between Banach spaces is open.

ContinuousLinearMap.isOpenMap.{u_1, u_2, u_3, u_4} {𝕜 : Type u_1} {𝕜' : Type u_2}
  [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3}
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜' F]
  (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ'] [RingHomIsometric σ] [RingHomIsometric σ']
  [CompleteSpace F] [CompleteSpace E] (surj : Function.Surjective ⇑f) : IsOpenMap ⇑f
Sources
MathlibContinuousLinearMap.isOpenMap
Uses 12
Statement usesCompleteness · Continuous linear map · Normed vector space over a normed field · Open map
Proof usesAbsolutely convergent series in Banach spaces · Baire theorem · Characteristic zero · Euclidean affine space · Hausdorff space · Metric structure · Squeeze theorem · Topology of a metric space

TheoremAbsolutely convergent series in Banach spaces#

Mathlib states this as Summable.of_norm.

Summable.of_norm.{u_1, u_3} {ι : Type u_1} {E : Type u_3} [SeminormedAddCommGroup E]
  [CompleteSpace E] {f : ι → E} (hf : Summable fun a => ‖f a‖) : Summable f
Sources
MathlibSummable.of_norm
Uses 7 · Used by 8
Statement usesBornology · Completeness · Infinite sum · Order
Proof usesCompleteness of R · Metric space · The Triangle Inequality
Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · Dirichlet’s Theorem · Banach open mapping theorem · Pentagonal number theorem · Poisson’s formula · Log · Continuity of the sum of a series of functions · Differentiability of the sum of a series of functions

TheoremHahn-Banach theorem#

Hahn-Banach theorem for continuous linear functions over 𝕜 satisfying IsRCLikeNormedField 𝕜.

exists_extension_norm_eq.{u_1, u_2} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  [IsRCLikeNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  (p : Subspace 𝕜 E) (f : StrongDual 𝕜 ↥p) : ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
Sources
Mathlibexists_extension_norm_eq
Uses 9 · Used by 1
Statement usesAssociative algebra over a commutative ring · Completeness · Dual of a normed space · Normed vector space over a normed field · Vector subspace
Proof usesDual vector space · Finite set · The Triangle Inequality · Topological ring
Used bySchwarz lemma

AbbreviationDual of a normed space#

The strong dual of a topological vector space M over a ring R. This is the space of continuous linear functionals and is equipped with the topology of uniform convergence on bounded subsets. StrongDual R M is an abbreviation for M →L[R] R.

StrongDual.{u_1, u_2} (R : Type u_1) [Semiring R] [TopologicalSpace R] (M : Type u_2)
  [TopologicalSpace M] [AddCommMonoid M] [_root_.Module R M] : Type (max u_1 u_2)
Sources
MathlibStrongDual
Uses 1 · Used by 13
Statement usesContinuous linear map
Used byFundamental Theorem of Integral Calculus · Local extrema · Eigenvalues from Rayleigh quotient · Fréchet-Riesz representation of the dual of a Hilbert space · Fundamental theorem of calculus, part 2 · Hahn-Banach theorem · Isometric inclusion in double dual · Gaussian measures · Darboux's theorem (analysis) · Rademacher's theorem · Banach–Alaoglu theorem · Krein–Milman theorem · Riemann-Lebesgue lemma (Measures and integral calculus)

DefinitionIsometric inclusion in double dual#

The inclusion of a normed space in its double strong dual is an isometry onto its image.

NormedSpace.inclusionInDoubleDualLi.{u, v} (𝕜 : Type v) [RCLike 𝕜] {E : Type u}
  [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : E →ₗᵢ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E)
Sources
MathlibNormedSpace.inclusionInDoubleDualLi
Uses 7
Statement usesAssociative algebra over a commutative ring · Completeness · Dual of a normed space · Finite set · Normed vector space over a normed field · Topological module · Topological ring

TheoremCompleteness of spaces of bounded continuous functions#

Bounded continuous functions taking values in a complete space form a complete space.

BoundedContinuousFunction.instCompleteSpace.{u, v} {α : Type u} {β : Type v} [TopologicalSpace α]
  [PseudoMetricSpace β] [CompleteSpace β] : CompleteSpace (BoundedContinuousFunction α β)
Sources
MathlibBoundedContinuousFunction.instCompleteSpace
Uses 9 · Used by 2
Statement usesBornology · Completeness · Continuous function · Order
Proof usesComplete metric spaces · Limits of sequences · Squeeze theorem · Uniform convergence · Uniformly continuous function
Used byArzela-Ascoli theorem · Tietze extension theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.