Adjoint of operators on Hilbert spaces #

Given an operator A : E →L[𝕜] F, where E and F are Hilbert spaces, its adjoint adjoint A : F →L[𝕜] E is the unique operator such that ⟪x, A y⟫ = ⟪adjoint A x, y⟫ for all x and y.

We then use this to put a C⋆-algebra structure on E →L[𝕜] E with the adjoint as the star operation.

This construction is used to define an adjoint for linear maps (i.e. not continuous) between finite dimensional spaces.

Main definitions #

ContinuousLinearMap.adjoint : (E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] (F →L[𝕜] E): the adjoint of a continuous linear map, bundled as a conjugate-linear isometric equivalence.
LinearMap.adjoint : (E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] (F →ₗ[𝕜] E): the adjoint of a linear map between finite-dimensional spaces, this time only as a conjugate-linear equivalence, since there is no norm defined on these maps.

Implementation notes #

The continuous conjugate-linear version adjointAux is only an intermediate definition and is not meant to be used outside this file.

Tags #

adjoint

Adjoint operator #

source

noncomputable def ContinuousLinearMap.adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] :

(E →L[𝕜] F) →L⋆[𝕜] F →L[𝕜] E

The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary definition for the main definition adjoint, where this is bundled as a conjugate-linear isometric equivalence.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem ContinuousLinearMap.adjointAux_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] (A : E →L[𝕜] F) (x : F) :

(ContinuousLinearMap.adjointAux A) x = (InnerProductSpace.toDual 𝕜 E).symm ((ContinuousLinearMap.toSesqForm A) x)

source

theorem ContinuousLinearMap.adjointAux_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] (A : E →L[𝕜] F) (x : E) (y : F) :

⟪(ContinuousLinearMap.adjointAux A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

source

theorem ContinuousLinearMap.adjointAux_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] (A : E →L[𝕜] F) (x : E) (y : F) :

⟪x, (ContinuousLinearMap.adjointAux A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

source

theorem ContinuousLinearMap.adjointAux_adjointAux {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :

ContinuousLinearMap.adjointAux (ContinuousLinearMap.adjointAux A) = A

source

@[simp]

theorem ContinuousLinearMap.adjointAux_norm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :

‖ContinuousLinearMap.adjointAux A‖ = ‖A‖

source

def ContinuousLinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] :

(E →L[𝕜] F) ≃ₗᵢ⋆[𝕜] F →L[𝕜] E

The adjoint of a bounded operator from Hilbert space E to Hilbert space F.

Equations

ContinuousLinearMap.adjoint = LinearIsometryEquiv.ofSurjective (let __src := ContinuousLinearMap.adjointAux; { toLinearMap := ↑__src, norm_map' := ⋯ }) ⋯

Instances For

source

def InnerProduct.«term_†» :

Lean.TrailingParserDescr

Equations

InnerProduct.«term_†» = Lean.ParserDescr.trailingNode `InnerProduct.term_† 1000 1000 (Lean.ParserDescr.symbol "†")

Instances For

source

theorem ContinuousLinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) (y : F) :

⟪(ContinuousLinearMap.adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

The fundamental property of the adjoint.

source

theorem ContinuousLinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) (y : F) :

⟪x, (ContinuousLinearMap.adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

The fundamental property of the adjoint.

source

@[simp]

theorem ContinuousLinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :

ContinuousLinearMap.adjoint (ContinuousLinearMap.adjoint A) = A

The adjoint is involutive.

source

@[simp]

theorem ContinuousLinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [InnerProductSpace 𝕜 G] [CompleteSpace E] [CompleteSpace G] [CompleteSpace F] (A : F →L[𝕜] G) (B : E →L[𝕜] F) :

ContinuousLinearMap.adjoint (A.comp B) = (ContinuousLinearMap.adjoint B).comp (ContinuousLinearMap.adjoint A)

The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.

source

theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) :

‖A x‖ ^ 2 = RCLike.re ⟪((ContinuousLinearMap.adjoint A).comp A) x, x⟫_𝕜

source

theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) :

‖A x‖ = √(RCLike.re ⟪((ContinuousLinearMap.adjoint A).comp A) x, x⟫_𝕜)

source

theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) :

‖A x‖ ^ 2 = RCLike.re ⟪x, ((ContinuousLinearMap.adjoint A).comp A) x⟫_𝕜

source

theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) :

‖A x‖ = √(RCLike.re ⟪x, ((ContinuousLinearMap.adjoint A).comp A) x⟫_𝕜)

source

theorem ContinuousLinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (B : F →L[𝕜] E) :

A = ContinuousLinearMap.adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all x and y.

source

@[simp]

theorem ContinuousLinearMap.adjoint_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

ContinuousLinearMap.adjoint (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 E

source

theorem Submodule.adjoint_subtypeL {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [CompleteSpace ↥U] :

ContinuousLinearMap.adjoint U.subtypeL = orthogonalProjection U

source

theorem Submodule.adjoint_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [CompleteSpace ↥U] :

ContinuousLinearMap.adjoint (orthogonalProjection U) = U.subtypeL

source

instance ContinuousLinearMap.instStarId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

Star (E →L[𝕜] E)

E →L[𝕜] E is a star algebra with the adjoint as the star operation.

Equations

ContinuousLinearMap.instStarId = { star := ⇑ContinuousLinearMap.adjoint }

source

instance ContinuousLinearMap.instInvolutiveStarId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

InvolutiveStar (E →L[𝕜] E)

Equations

ContinuousLinearMap.instInvolutiveStarId = InvolutiveStar.mk ⋯

source

instance ContinuousLinearMap.instStarMulId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

StarMul (E →L[𝕜] E)

Equations

ContinuousLinearMap.instStarMulId = StarMul.mk ⋯

source

instance ContinuousLinearMap.instStarRingId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

StarRing (E →L[𝕜] E)

Equations

ContinuousLinearMap.instStarRingId = StarRing.mk ⋯

source

instance ContinuousLinearMap.instStarModuleId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

StarModule 𝕜 (E →L[𝕜] E)

Equations

⋯ = ⋯

source

theorem ContinuousLinearMap.star_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (A : E →L[𝕜] E) :

star A = ContinuousLinearMap.adjoint A

source

theorem ContinuousLinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} :

IsSelfAdjoint A ↔ ContinuousLinearMap.adjoint A = A

A continuous linear operator is self-adjoint iff it is equal to its adjoint.

source

theorem ContinuousLinearMap.norm_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :

‖(ContinuousLinearMap.adjoint A).comp A‖ = ‖A‖ * ‖A‖

source

instance ContinuousLinearMap.instCstarRingId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

CstarRing (E →L[𝕜] E)

Equations

⋯ = ⋯

source

theorem ContinuousLinearMap.isAdjointPair_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) :

sesqFormOfInner.IsAdjointPair sesqFormOfInner ↑A ↑(ContinuousLinearMap.adjoint A)

Self-adjoint operators #

source

theorem IsSelfAdjoint.adjoint_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} (hA : IsSelfAdjoint A) :

ContinuousLinearMap.adjoint A = A

source

theorem IsSelfAdjoint.isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} (hA : IsSelfAdjoint A) :

(↑A).IsSymmetric

Every self-adjoint operator on an inner product space is symmetric.

source

theorem IsSelfAdjoint.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : E →L[𝕜] F) :

IsSelfAdjoint (S.comp (T.comp (ContinuousLinearMap.adjoint S)))

Conjugating preserves self-adjointness.

source

theorem IsSelfAdjoint.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : F →L[𝕜] E) :

IsSelfAdjoint ((ContinuousLinearMap.adjoint S).comp (T.comp S))

Conjugating preserves self-adjointness.

source

theorem ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} :

IsSelfAdjoint A ↔ (↑A).IsSymmetric

source

theorem LinearMap.IsSymmetric.isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} (hA : (↑A).IsSymmetric) :

IsSelfAdjoint A

source

theorem orthogonalProjection_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [CompleteSpace ↥U] :

IsSelfAdjoint (U.subtypeL.comp (orthogonalProjection U))

The orthogonal projection is self-adjoint.

source

theorem IsSelfAdjoint.conj_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (U : Submodule 𝕜 E) [CompleteSpace ↥U] :

IsSelfAdjoint (U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U)))))

source

def LinearMap.IsSymmetric.toSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :

↥(selfAdjoint (E →L[𝕜] E))

The Hellinger--Toeplitz theorem: Construct a self-adjoint operator from an everywhere defined symmetric operator.

Equations

hT.toSelfAdjoint = ⟨{ toLinearMap := T, cont := ⋯ }, ⋯⟩

Instances For

source

theorem LinearMap.IsSymmetric.coe_toSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :

↑↑hT.toSelfAdjoint = T

source

theorem LinearMap.IsSymmetric.toSelfAdjoint_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {x : E} :

↑hT.toSelfAdjoint x = T x

source

def LinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] :

(E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] F →ₗ[𝕜] E

The adjoint of an operator from the finite-dimensional inner product space E to the finite-dimensional inner product space F.

Equations

LinearMap.adjoint = let_fun this := ⋯; let_fun this_1 := ⋯; (LinearMap.toContinuousLinearMap.trans ContinuousLinearMap.adjoint.toLinearEquiv).trans LinearMap.toContinuousLinearMap.symm

Instances For

source

theorem LinearMap.adjoint_toContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) :

LinearMap.toContinuousLinearMap (LinearMap.adjoint A) = ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A)

source

theorem LinearMap.adjoint_eq_toCLM_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) :

LinearMap.adjoint A = ↑(ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A))

source

theorem LinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) (y : F) :

⟪(LinearMap.adjoint A) y, x⟫_𝕜 = ⟪y, A x⟫_𝕜

The fundamental property of the adjoint.

source

theorem LinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (x : E) (y : F) :

⟪x, (LinearMap.adjoint A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

The fundamental property of the adjoint.

source

@[simp]

theorem LinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) :

LinearMap.adjoint (LinearMap.adjoint A) = A

The adjoint is involutive.

source

@[simp]

theorem LinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] (A : F →ₗ[𝕜] G) (B : E →ₗ[𝕜] F) :

LinearMap.adjoint (A ∘ₗ B) = LinearMap.adjoint B ∘ₗ LinearMap.adjoint A

The adjoint of the composition of two operators is the composition of the two adjoints in reverse order.

source

theorem LinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :

A = LinearMap.adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜

The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all x and y.

source

theorem LinearMap.eq_adjoint_iff_basis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι₁ : Type u_5} {ι₂ : Type u_6} (b₁ : Basis ι₁ 𝕜 E) (b₂ : Basis ι₂ 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :

A = LinearMap.adjoint B ↔ ∀ (i₁ : ι₁) (i₂ : ι₂), ⟪A (b₁ i₁), b₂ i₂⟫_𝕜 = ⟪b₁ i₁, B (b₂ i₂)⟫_𝕜

The adjoint is unique: a map A is the adjoint of B iff it satisfies ⟪A x, y⟫ = ⟪x, B y⟫ for all basis vectors x and y.

source

theorem LinearMap.eq_adjoint_iff_basis_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι : Type u_5} (b : Basis ι 𝕜 E) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :

A = LinearMap.adjoint B ↔ ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜

source

theorem LinearMap.eq_adjoint_iff_basis_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι : Type u_5} (b : Basis ι 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :

A = LinearMap.adjoint B ↔ ∀ (i : ι) (x : E), ⟪A x, b i⟫_𝕜 = ⟪x, B (b i)⟫_𝕜

source

instance LinearMap.instStarId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

Star (E →ₗ[𝕜] E)

E →ₗ[𝕜] E is a star algebra with the adjoint as the star operation.

Equations

LinearMap.instStarId = { star := ⇑LinearMap.adjoint }

source

instance LinearMap.instInvolutiveStarId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

InvolutiveStar (E →ₗ[𝕜] E)

Equations

LinearMap.instInvolutiveStarId = InvolutiveStar.mk ⋯

source

instance LinearMap.instStarMulId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

StarMul (E →ₗ[𝕜] E)

Equations

LinearMap.instStarMulId = StarMul.mk ⋯

source

instance LinearMap.instStarRingId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

StarRing (E →ₗ[𝕜] E)

Equations

LinearMap.instStarRingId = StarRing.mk ⋯

source

instance LinearMap.instStarModuleId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

StarModule 𝕜 (E →ₗ[𝕜] E)

Equations

⋯ = ⋯

source

theorem LinearMap.star_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) :

star A = LinearMap.adjoint A

source

theorem LinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} :

IsSelfAdjoint A ↔ LinearMap.adjoint A = A

A continuous linear operator is self-adjoint iff it is equal to its adjoint.

source

theorem LinearMap.isSymmetric_iff_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (A : E →ₗ[𝕜] E) :

A.IsSymmetric ↔ IsSelfAdjoint A

source

theorem LinearMap.isAdjointPair_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) :

sesqFormOfInner.IsAdjointPair sesqFormOfInner A (LinearMap.adjoint A)

source

theorem LinearMap.isSymmetric_adjoint_mul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) :

(LinearMap.adjoint T * T).IsSymmetric

The Gram operator T†T is symmetric.

source

theorem LinearMap.re_inner_adjoint_mul_self_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E) :

0 ≤ RCLike.re ⟪x, (LinearMap.adjoint T * T) x⟫_𝕜

The Gram operator T†T is a positive operator.

source

@[simp]

theorem LinearMap.im_inner_adjoint_mul_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E) :

RCLike.im ⟪x, (LinearMap.adjoint T) (T x)⟫_𝕜 = 0

source

theorem ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {K : Type u_6} [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (u : H →L[𝕜] K) :

(∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜) ↔ (ContinuousLinearMap.adjoint u).comp u = 1

source

theorem ContinuousLinearMap.norm_map_iff_adjoint_comp_self {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {K : Type u_6} [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (u : H →L[𝕜] K) :

(∀ (x : H), ‖u x‖ = ‖x‖) ↔ (ContinuousLinearMap.adjoint u).comp u = 1

source

@[simp]

theorem LinearIsometryEquiv.adjoint_eq_symm {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {K : Type u_6} [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (e : H ≃ₗᵢ[𝕜] K) :

ContinuousLinearMap.adjoint ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

source

@[simp]

theorem LinearIsometryEquiv.star_eq_symm {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (e : H ≃ₗᵢ[𝕜] H) :

star ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ↑{ toLinearEquiv := e.symm.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

source

theorem ContinuousLinearMap.norm_map_of_mem_unitary {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {u : H →L[𝕜] H} (hu : u ∈ unitary (H →L[𝕜] H)) (x : H) :

‖u x‖ = ‖x‖

source

theorem ContinuousLinearMap.inner_map_map_of_mem_unitary {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] {u : H →L[𝕜] H} (hu : u ∈ unitary (H →L[𝕜] H)) (x : H) (y : H) :

⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜

source

theorem unitary.norm_map {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (u : ↥(unitary (H →L[𝕜] H))) (x : H) :

‖↑u x‖ = ‖x‖

source

theorem unitary.inner_map_map {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (u : ↥(unitary (H →L[𝕜] H))) (x : H) (y : H) :

⟪↑u x, ↑u y⟫_𝕜 = ⟪x, y⟫_𝕜

source

noncomputable def unitary.linearIsometryEquiv {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] :

↥(unitary (H →L[𝕜] H)) ≃* (H ≃ₗᵢ[𝕜] H)

The unitary elements of continuous linear maps on a Hilbert space coincide with the linear isometric equivalences on that Hilbert space.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem unitary.linearIsometryEquiv_coe_apply {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (u : ↥(unitary (H →L[𝕜] H))) :

↑{ toLinearEquiv := (unitary.linearIsometryEquiv u).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ↑u

source

@[simp]

theorem unitary.linearIsometryEquiv_coe_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (e : H ≃ₗᵢ[𝕜] H) :

↑(unitary.linearIsometryEquiv.symm e) = ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

source

theorem Matrix.toLin_conjTranspose {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] {m : Type u_5} {n : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (v₁ : OrthonormalBasis n 𝕜 E) (v₂ : OrthonormalBasis m 𝕜 F) (A : Matrix m n 𝕜) :

(Matrix.toLin v₂.toBasis v₁.toBasis) A.conjTranspose = LinearMap.adjoint ((Matrix.toLin v₁.toBasis v₂.toBasis) A)

The linear map associated to the conjugate transpose of a matrix corresponding to two orthonormal bases is the adjoint of the linear map associated to the matrix.

source

theorem LinearMap.toMatrix_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] {m : Type u_5} {n : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (v₁ : OrthonormalBasis n 𝕜 E) (v₂ : OrthonormalBasis m 𝕜 F) (f : E →ₗ[𝕜] F) :

(LinearMap.toMatrix v₂.toBasis v₁.toBasis) (LinearMap.adjoint f) = ((LinearMap.toMatrix v₁.toBasis v₂.toBasis) f).conjTranspose

The matrix associated to the adjoint of a linear map corresponding to two orthonormal bases is the conjugate tranpose of the matrix associated to the linear map.

source

@[simp]

theorem LinearMap.toMatrixOrthonormal_symm_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : Type u_6} [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] (v₁ : OrthonormalBasis n 𝕜 E) :

∀ (a : Matrix n n 𝕜), (LinearMap.toMatrixOrthonormal v₁).symm a = (LinearMap.toMatrix v₁.toBasis v₁.toBasis).invFun a

source

@[simp]

theorem LinearMap.toMatrixOrthonormal_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : Type u_6} [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] (v₁ : OrthonormalBasis n 𝕜 E) :

∀ (a : E →ₗ[𝕜] E), (LinearMap.toMatrixOrthonormal v₁) a = (↑(LinearMap.toMatrix v₁.toBasis v₁.toBasis)).toFun a

source

def LinearMap.toMatrixOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : Type u_6} [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] (v₁ : OrthonormalBasis n 𝕜 E) :

(E →ₗ[𝕜] E) ≃⋆ₐ[𝕜] Matrix n n 𝕜

The star algebra equivalence between the linear endomorphisms of finite-dimensional inner product space and square matrices induced by the choice of an orthonormal basis.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint {𝕜 : Type u_1} [RCLike 𝕜] {m : Type u_5} {n : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) :

Matrix.toEuclideanLin A.conjTranspose = LinearMap.adjoint (Matrix.toEuclideanLin A)

The adjoint of the linear map associated to a matrix is the linear map associated to the conjugate transpose of that matrix.

Documentation

Mathlib.Analysis.InnerProductSpace.Adjoint

Adjoint of operators on Hilbert spaces #

Main definitions #

Implementation notes #

Tags #

Adjoint operator #

Self-adjoint operators #