Hilbert spaces

ClassInner product space, over \(R\) or \(C\)#

A (pre) inner product space is a vector space with an additional operation called inner product. The (semi)norm could be derived from the inner product, instead we require the existence of a seminorm and the fact that ‖x‖^2 = re ⟪x, x⟫ to be able to put instances on 𝕂 or product spaces.

Note that NormedSpace does not assume that ‖x‖=0 implies x=0 (it is rather a seminorm).

To construct a seminorm from an inner product, see PreInnerProductSpace.ofCore.

InnerProductSpace.{u_4, u_5} (𝕜 : Type u_4) (E : Type u_5) [RCLike 𝕜] [SeminormedAddCommGroup E] :
  Type (max u_4 u_5)
Sources
MathlibInnerProductSpace
Uses 3 · Used by 48
Statement usesAssociative algebra over a commutative ring · Completeness · Normed vector space over a normed field
Used byFourier Series · Analyticity of holomorphic functions · Phragmen-Lindelöf principle · Jensen's inequality (integral version) · Distributions · Tempered distributions · Fourier transform as an integral · Inversion formula · Riemann-Lebesgue lemma (Analysis) · Cauchy-Schwarz inequality · Eigenvalues from Rayleigh quotient · Fréchet-Riesz representation of the dual of a Hilbert space · Orthogonal complement · Lebesgue measure (Measures and integral calculus) · Approximation by convolution · Fubini's theorem · Regularization by convolution · Behrend's construction · Angle · Sphere · Closed interval · Riemannian manifold · Smooth bundle metric · Existence of orthonormal basis · Characteristic function · Mean of product of independent random variables · Moment of a random variable · Variance of a real-valued random variable · Prokhorov's theorem · Gauss–Lucas theorem · Hadamard three-lines theorem · Open mapping theorem (complex analysis) · Fourier theorem · Hellinger–Toeplitz theorem · Apollonius's theorem · Whitney embedding theorem · Slutsky's theorem · Orthonormal bases · Poisson’s formula · Convolution of two functions of \(\mathcal{S}(\R^d)\) · Fourier transforms on \(\mathcal{S}(\R^d)\) · Fourier transform on \(\mathrm{L}^2(\R^d)\) · Plancherel’s theorem · Taylor's theorem with Lagrange form for remainder · Hilbert bases · Hilbert projection theorem · Inner product space \(l^2\) · Inner product space \(L^2\)

TheoremCauchy-Schwarz inequality#

Cauchy–Schwarz inequality.

inner_mul_inner_self_le.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :
  ‖inner 𝕜 x y‖ * ‖inner 𝕜 y x‖ ≤ RCLike.re (inner 𝕜 x x) * RCLike.re (inner 𝕜 y y)

Freek Wiedijk's list (no. 78) also cites norm_inner_le_norm.

Sources
Mathlibinner_mul_inner_self_le
Uses 1 · Used by 1
Statement usesInner product space, over \(R\) or \(C\)
Used bySum of the Angles of a Triangle

DefinitionAdjoint operator#

The adjoint operator as a partially defined linear operator, denoted as T†.

LinearPMap.adjoint.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  (T : E →ₗ.[𝕜] F) [CompleteSpace E] : F →ₗ.[𝕜] E
Sources
MathlibLinearPMap.adjoint
Uses 2
Statement usesExtension by continuity · Fréchet-Riesz representation of the dual of a Hilbert space

DefinitionSelf-adjoint operator#

An element is self-adjoint if it is equal to its star.

IsSelfAdjoint.{u_1} {R : Type u_1} [Star R] (x : R) : Prop
Sources
MathlibIsSelfAdjoint
Used by 1
Used byEigenvalues from Rayleigh quotient

DefinitionOrthogonal projection#

The orthogonal projection onto a subspace.

Submodule.orthogonalProjectionOnto.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] :
  E →L[𝕜] ↥K
Sources
MathlibSubmodule.orthogonalProjectionOnto
Uses 5 · Used by 4
Statement usesContinuous linear map · Orthogonal complement · Product of vector spaces · Range of a linear map · Sum of subspaces
Used byReflection · Sphere · Conditional expectation · Gram-Schmidt orthogonalisation

DefinitionReflection#

Reflection in a complete subspace of an inner product space. The word "reflection" is sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes more generally to cover operations such as reflection in a point. The definition here, of reflection in a subspace, is a more general sense of the word that includes both those common cases.

Submodule.reflection.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] : E ≃ₗᵢ[𝕜] E
Sources
MathlibSubmodule.reflection
Uses 1 · Used by 1
Statement usesOrthogonal projection
Used byDecomposition of an orthogonal transformation as a product of reflections

DefinitionOrthogonal complement#

The subspace of vectors orthogonal to a given subspace, denoted Kᗮ.

Submodule.orthogonal.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] (K : Submodule 𝕜 E) : Submodule 𝕜 E
Sources
MathlibSubmodule.orthogonal
Uses 1 · Used by 5
Statement usesInner product space, over \(R\) or \(C\)
Used byExistence of Hilbert basis · Orthogonal projection · Diagonalization of self-adjoint endomorphisms · Tangent-secant theorem · Orthonormal bases

TheoremExistence of Hilbert basis#

A Hilbert space admits a Hilbert basis.

exists_hilbertBasis.{u_2, u_3} (𝕜 : Type u_2) [RCLike 𝕜] (E : Type u_3) [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [CompleteSpace E] : ∃ w b, ⇑b = Subtype.val
Sources
Mathlibexists_hilbertBasis
Uses 10
Statement usesHilbert bases
Proof usesClosure · Completeness of \(l^2\) · Completeness of R · Generating sets · Hausdorff space · Orthogonal complement · Range of a linear map · Sum of subspaces · Topology on a normed vector space

TheoremEigenvalues from Rayleigh quotient#

For a self-adjoint operator T, a local extremum of the Rayleigh quotient of T on a sphere centred at the origin is an eigenvector of T.

IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2}
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E}
  (hT : IsSelfAdjoint T) {x₀ : E} (hx₀ : x₀ ≠ 0)
  (hextr : IsLocalExtrOn T.reApplyInnerSelf (Metric.sphere 0 ‖x₀‖) x₀) :
  Module.End.HasEigenvector (↑T) (↑(T.rayleighQuotient x₀)) x₀
Sources
MathlibIsSelfAdjoint.hasEigenvector_of_isLocalExtrOn
Uses 11 · Used by 1
Statement usesContinuous linear map · Eigenvector · Inner product space, over \(R\) or \(C\) · Self-adjoint operator
Proof usesCharacteristic zero · Completeness of R · Dual of a normed space · Finite set · Hellinger–Toeplitz theorem · Topological module · Topological ring
Used byDiagonalization of self-adjoint endomorphisms

DefinitionFréchet-Riesz representation of the dual of a Hilbert space#

Fréchet-Riesz representation: any ℓ in the dual of a Hilbert space E is of the form fun u => ⟪y, u⟫ for some y : E, i.e. toDualMap is surjective.

InnerProductSpace.toDual.{u_1, u_2} (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [CompleteSpace E] : E ≃ₗᵢ⋆[𝕜] StrongDual 𝕜 E
Sources
MathlibInnerProductSpace.toDual
Uses 4 · Used by 4
Statement usesDual of a normed space · Inner product space, over \(R\) or \(C\) · Range of a linear map · Topological ring
Used byAdjoint operator · Lax-Milgram theorem · Riemann-Lebesgue lemma (Measures and integral calculus) · Gradient vector

DefinitionLax-Milgram theorem#

The Lax-Milgram equivalence of a coercive bounded bilinear operator: for all v : V, continuousLinearEquivOfBilin B v is the unique element V such that continuousLinearEquivOfBilin B v, w⟫ = B v w. The Lax-Milgram theorem states that this is a continuous equivalence.

IsCoercive.continuousLinearEquivOfBilin.{u} {V : Type u} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (coercive : IsCoercive B) :
  V ≃L[ℝ] V
Sources
MathlibIsCoercive.continuousLinearEquivOfBilin
Uses 3
Statement usesFréchet-Riesz representation of the dual of a Hilbert space · Homeomorphisms · Kernel of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.