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

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.

@[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) : (adjointAux A) x = (InnerProductSpace.toDual 𝕜 E).symm ((toSesqForm A) x)

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) : inner ((adjointAux A) y) x = inner y (A x)

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) : inner x ((adjointAux A) y) = inner (A x) y

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) : adjointAux (adjointAux A) = A

@[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) : ‖adjointAux A‖ = ‖A‖

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 A from a Hilbert space E to another Hilbert space F, denoted as A†.

Equations

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

def InnerProduct.«term_†» : Lean.TrailingParserDescr

The adjoint of a bounded operator A from a Hilbert space E to another Hilbert space F, denoted as A†.

Equations

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

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) : inner ((adjoint A) y) x = inner y (A x)

The fundamental property of the adjoint.

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) : inner x ((adjoint A) y) = inner (A x) y

The fundamental property of the adjoint.

@[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) : adjoint (adjoint A) = A

The adjoint is involutive.

@[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) : adjoint (A.comp B) = (adjoint B).comp (adjoint A)

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

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 (inner (((adjoint A).comp A) x) x)

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 (inner (((adjoint A).comp A) x) x))

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 (inner x (((adjoint A).comp A) x))

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 (inner x (((adjoint A).comp A) x)))

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 = adjoint B ↔ ∀ (x : E) (y : F), inner (A x) y = inner 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.

@[simp]

theorem ContinuousLinearMap.adjoint_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : adjoint (id 𝕜 E) = id 𝕜 E

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

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

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 }

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 ⋯

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 ⋯

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 ⋯

instance ContinuousLinearMap.instStarModuleId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : StarModule 𝕜 (E →L[𝕜] E)

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 = adjoint A

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

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

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) : ‖(adjoint A).comp A‖ = ‖A‖ * ‖A‖

instance ContinuousLinearMap.instCStarRingId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : CStarRing (E →L[𝕜] E)

The C⋆-algebra instance when 𝕜 := ℂ can be found in Analysis.CStarAlgebra.ContinuousLinearMap.

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 ⇑(adjoint A)

Self-adjoint operators

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

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.

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.

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.

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

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

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.

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)))))

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 := ⋯ }, ⋯⟩

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

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

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 = (LinearMap.toContinuousLinearMap.trans ContinuousLinearMap.adjoint.toLinearEquiv).trans LinearMap.toContinuousLinearMap.symm

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) : toContinuousLinearMap (adjoint A) = ContinuousLinearMap.adjoint (toContinuousLinearMap A)

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) : adjoint A = ↑(ContinuousLinearMap.adjoint (toContinuousLinearMap A))

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) : inner ((adjoint A) y) x = inner y (A x)

The fundamental property of the adjoint.

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) : inner x ((adjoint A) y) = inner (A x) y

The fundamental property of the adjoint.

@[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) : adjoint (adjoint A) = A

The adjoint is involutive.

@[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) : adjoint (A ∘ₗ B) = adjoint B ∘ₗ adjoint A

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

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 = adjoint B ↔ ∀ (x : E) (y : F), inner (A x) y = inner 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.

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 = adjoint B ↔ ∀ (i₁ : ι₁) (i₂ : ι₂), inner (A (b₁ i₁)) (b₂ i₂) = inner (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.

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 = adjoint B ↔ ∀ (i : ι) (y : F), inner (A (b i)) y = inner (b i) (B y)

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 = adjoint B ↔ ∀ (i : ι) (x : E), inner (A x) (b i) = inner x (B (b i))

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 }

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 ⋯

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 ⋯

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 ⋯

instance LinearMap.instStarModuleId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : StarModule 𝕜 (E →ₗ[𝕜] E)

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

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

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

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

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 ⇑(adjoint A)

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

The Gram operator T†T is symmetric.

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 (inner x ((adjoint T * T) x))

The Gram operator T†T is a positive operator.

@[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 (inner x ((adjoint T) (T x))) = 0

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), inner (u x) (u y) = inner x y) ↔ (adjoint u).comp u = 1

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‖) ↔ (adjoint u).comp u = 1

@[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 := ⋯ }

@[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 := ⋯ }

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‖

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 y : H) : inner (u x) (u y) = inner x y

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‖

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 y : H) : inner (↑u x) (↑u y) = inner x y

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.

@[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 := (linearIsometryEquiv u).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ↑u

@[simp]

theorem unitary.linearIsometryEquiv_coe_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (e : H ≃ₗᵢ[𝕜] H) : ↑(linearIsometryEquiv.symm e) = ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

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 𝕜) : (toLin v₂.toBasis v₁.toBasis) A.conjTranspose = LinearMap.adjoint ((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.

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) : (toMatrix v₂.toBasis v₁.toBasis) (adjoint f) = ((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 transpose of the matrix associated to the linear map.

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.

@[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) : (toMatrixOrthonormal v₁) a✝ = (↑(toMatrix v₁.toBasis v₁.toBasis)).toFun a✝

@[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 𝕜) : (toMatrixOrthonormal v₁).symm a✝ = (toMatrix v₁.toBasis v₁.toBasis).invFun a✝

theorem LinearMap.toMatrixOrthonormal_apply_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) (f : E →ₗ[𝕜] E) (i j : n) : (toMatrixOrthonormal v₁) f i j = inner (v₁ i) (f (v₁ j))

theorem LinearMap.toMatrixOrthonormal_reindex {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {m : Type u_5} {n : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] (v₁ : OrthonormalBasis n 𝕜 E) (e : n ≃ m) (f : E →ₗ[𝕜] E) : (toMatrixOrthonormal (v₁.reindex e)) f = (Matrix.reindex e e) ((toMatrixOrthonormal v₁) f)

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 𝕜) : toEuclideanLin A.conjTranspose = LinearMap.adjoint (toEuclideanLin A)

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