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} [IsROrC 𝕜] [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} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] (A : E →L[𝕜] F) (x : F) : (ContinuousLinearMap.adjointAux A) x = (LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) ((ContinuousLinearMap.toSesqForm A) x)

theorem ContinuousLinearMap.adjointAux_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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⟫_𝕜

theorem ContinuousLinearMap.adjointAux_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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⟫_𝕜

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

@[simp]

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

def ContinuousLinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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

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

def InnerProduct.«term_†» : Lean.TrailingParserDescr

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} [IsROrC 𝕜] [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.

theorem ContinuousLinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.

@[simp]

theorem ContinuousLinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.

@[simp]

theorem ContinuousLinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [IsROrC 𝕜] [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 (ContinuousLinearMap.comp A B) = ContinuousLinearMap.comp (ContinuousLinearMap.adjoint B) (ContinuousLinearMap.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} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) : ‖A x‖ ^ 2 = IsROrC.re ⟪(ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A) x, x⟫_𝕜

theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) : ‖A x‖ = Real.sqrt (IsROrC.re ⟪(ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A) x, x⟫_𝕜)

theorem ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) : ‖A x‖ ^ 2 = IsROrC.re ⟪x, (ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A) x⟫_𝕜

theorem ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) (x : E) : ‖A x‖ = Real.sqrt (IsROrC.re ⟪x, (ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A) x⟫_𝕜)

theorem ContinuousLinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.

@[simp]

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

theorem Submodule.adjoint_subtypeL {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [CompleteSpace ↥U] : ContinuousLinearMap.adjoint (Submodule.subtypeL U) = orthogonalProjection U

theorem Submodule.adjoint_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [CompleteSpace ↥U] : ContinuousLinearMap.adjoint (orthogonalProjection U) = Submodule.subtypeL U

instance ContinuousLinearMap.instStarContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToNormedSpace {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [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

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

instance ContinuousLinearMap.instInvolutiveStarContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToNormedSpace {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : InvolutiveStar (E →L[𝕜] E)

Equations

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

instance ContinuousLinearMap.instStarMulContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToNormedSpaceInstMul {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : StarMul (E →L[𝕜] E)

Equations

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

instance ContinuousLinearMap.instStarRingContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToNormedSpaceToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingRingToRingToNormedRingToNormedCommRingToAddCommGroupToTopologicalAddGroup {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : StarRing (E →L[𝕜] E)

Equations

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

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

Equations

• (_ : StarModule 𝕜 (E →L[𝕜] E)) = (_ : StarModule 𝕜 (E →L[𝕜] E))

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

theorem ContinuousLinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [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.

theorem ContinuousLinearMap.norm_adjoint_comp_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) : ‖ContinuousLinearMap.comp (ContinuousLinearMap.adjoint A) A‖ = ‖A‖ * ‖A‖

instance ContinuousLinearMap.instCstarRingContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToNormedSpaceToNonUnitalNormedRingToNormedRingToNontriviallyNormedFieldInstStarRingContinuousLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedAddCommGroupToAddCommMonoidToAddCommGroupToModuleToNormedSpaceToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingRingToRingToNormedRingToNormedCommRingToAddCommGroupToTopologicalAddGroup {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : CstarRing (E →L[𝕜] E)

Equations

• (_ : CstarRing (E →L[𝕜] E)) = (_ : CstarRing (E →L[𝕜] E))

theorem ContinuousLinearMap.isAdjointPair_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (A : E →L[𝕜] F) : LinearMap.IsAdjointPair sesqFormOfInner sesqFormOfInner ↑A ↑(ContinuousLinearMap.adjoint A)

Self-adjoint operators

theorem IsSelfAdjoint.adjoint_eq {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [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} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} (hA : IsSelfAdjoint A) : LinearMap.IsSymmetric ↑A

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} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : E →L[𝕜] F) : IsSelfAdjoint (ContinuousLinearMap.comp S (ContinuousLinearMap.comp T (ContinuousLinearMap.adjoint S)))

Conjugating preserves self-adjointness.

theorem IsSelfAdjoint.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.comp (ContinuousLinearMap.adjoint S) (ContinuousLinearMap.comp T S))

Conjugating preserves self-adjointness.

theorem ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} : IsSelfAdjoint A ↔ LinearMap.IsSymmetric ↑A

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

theorem orthogonalProjection_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [CompleteSpace ↥U] : IsSelfAdjoint (ContinuousLinearMap.comp (Submodule.subtypeL U) (orthogonalProjection U))

The orthogonal projection is self-adjoint.

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

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

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

Equations

• LinearMap.IsSymmetric.toSelfAdjoint hT = { val := ContinuousLinearMap.mk T, property := (_ : IsSelfAdjoint (ContinuousLinearMap.mk T)) }

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

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

def LinearMap.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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

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

theorem LinearMap.adjoint_toContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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)

theorem LinearMap.adjoint_eq_toCLM_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : LinearMap.adjoint A = ↑(ContinuousLinearMap.adjoint (LinearMap.toContinuousLinearMap A))

theorem LinearMap.adjoint_inner_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.

theorem LinearMap.adjoint_inner_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.

@[simp]

theorem LinearMap.adjoint_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.

@[simp]

theorem LinearMap.adjoint_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [IsROrC 𝕜] [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.

theorem LinearMap.eq_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.

theorem LinearMap.eq_adjoint_iff_basis {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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.

theorem LinearMap.eq_adjoint_iff_basis_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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⟫_𝕜

theorem LinearMap.eq_adjoint_iff_basis_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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)⟫_𝕜

instance LinearMap.instStarLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToAddCommMonoidToAddCommGroupToModuleToSeminormedAddCommGroupToNormedSpace {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : Star (E →ₗ[𝕜] E)

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

Equations

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

instance LinearMap.instInvolutiveStarLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToAddCommMonoidToAddCommGroupToModuleToSeminormedAddCommGroupToNormedSpace {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : InvolutiveStar (E →ₗ[𝕜] E)

Equations

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

instance LinearMap.instStarMulLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToAddCommMonoidToAddCommGroupToModuleToSeminormedAddCommGroupToNormedSpaceInstMulEnd {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : StarMul (E →ₗ[𝕜] E)

Equations

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

instance LinearMap.instStarRingLinearMapToSemiringToDivisionSemiringToSemifieldToFieldToNormedFieldToDenselyNormedFieldIdToNonAssocSemiringToAddCommMonoidToAddCommGroupToModuleToSeminormedAddCommGroupToNormedSpaceToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingRingToAddCommGroup {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : StarRing (E →ₗ[𝕜] E)

Equations

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

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

Equations

• (_ : StarModule 𝕜 (E →ₗ[𝕜] E)) = (_ : StarModule 𝕜 (E →ₗ[𝕜] E))

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

theorem LinearMap.isSelfAdjoint_iff' {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [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.

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

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

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

The Gram operator T†T is symmetric.

theorem LinearMap.re_inner_adjoint_mul_self_nonneg {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E) : 0 ≤ IsROrC.re ⟪x, (LinearMap.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} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) (x : E) : IsROrC.im ⟪x, (LinearMap.adjoint T) (T x)⟫_𝕜 = 0

theorem Matrix.toLin_conjTranspose {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [IsROrC 𝕜] [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 (OrthonormalBasis.toBasis v₂) (OrthonormalBasis.toBasis v₁)) (Matrix.conjTranspose A) = LinearMap.adjoint ((Matrix.toLin (OrthonormalBasis.toBasis v₁) (OrthonormalBasis.toBasis v₂)) 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} [IsROrC 𝕜] [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 (OrthonormalBasis.toBasis v₂) (OrthonormalBasis.toBasis v₁)) (LinearMap.adjoint f) = Matrix.conjTranspose ((LinearMap.toMatrix (OrthonormalBasis.toBasis v₁) (OrthonormalBasis.toBasis v₂)) f)

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.

@[simp]

theorem LinearMap.toMatrixOrthonormal_apply {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [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 (OrthonormalBasis.toBasis v₁) (OrthonormalBasis.toBasis v₁))).toAddHom.toFun a

@[simp]

theorem LinearMap.toMatrixOrthonormal_symm_apply {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : Type u_6} [Fintype n] [DecidableEq n] [FiniteDimensional 𝕜 E] (v₁ : OrthonormalBasis n 𝕜 E) : ∀ (a : Matrix n n 𝕜), (StarAlgEquiv.symm (LinearMap.toMatrixOrthonormal v₁)) a = (LinearMap.toMatrix (OrthonormalBasis.toBasis v₁) (OrthonormalBasis.toBasis v₁)).invFun a

def LinearMap.toMatrixOrthonormal {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [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.

theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint {𝕜 : Type u_1} [IsROrC 𝕜] {m : Type u_5} {n : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (A : Matrix m n 𝕜) : Matrix.toEuclideanLin (Matrix.conjTranspose A) = 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.