# 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) :
(adjointAux A) x = (InnerProductSpace.toDual 𝕜 E).symm ((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) :
inner 𝕜 ((adjointAux A) y) x = inner 𝕜 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) :
inner 𝕜 x ((adjointAux A) y) = inner 𝕜 (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) :
adjointAux (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) :
‖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 `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' := ⋯ }) ⋯

Instances For

source
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 "†")

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

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 (inner 𝕜 (((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 (inner 𝕜 (((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 (inner 𝕜 x (((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 (inner 𝕜 x (((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 = 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`.

source
@[simp]
theorem LinearMap.IsSymmetric.clm_adjoint_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} (hA : (↑A).IsSymmetric) :
ContinuousLinearMap.adjoint A = A
source
theorem ContinuousLinearMap.adjoint_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :
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 = U.orthogonalProjection
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 U.orthogonalProjection = U.subtypeL
source
theorem ContinuousLinearMap.orthogonal_ker {𝕜 : 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[𝕜] F) :
(LinearMap.ker T)ᗮ = (LinearMap.range (adjoint T)).topologicalClosure
source
theorem ContinuousLinearMap.orthogonal_range {𝕜 : 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[𝕜] F) :
(LinearMap.range T)ᗮ = LinearMap.ker (adjoint T)
source
theorem ContinuousLinearMap.ker_le_ker_iff_range_le_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T U : E →L[𝕜] E} (hT : (↑T).IsSymmetric) (hU : (↑U).IsSymmetric) :
LinearMap.ker U ≤ LinearMap.ker T ↔ LinearMap.range T ≤ LinearMap.range U
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 = { toStar := ContinuousLinearMap.instStarId, star_involutive := ⋯ }

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 = { toInvolutiveStar := ContinuousLinearMap.instInvolutiveStarId, star_mul := ⋯ }

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 = { toStarMul := ContinuousLinearMap.instStarMulId, star_add := ⋯ }

source
instance ContinuousLinearMap.instStarModuleId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :
StarModule 𝕜 (E →L[𝕜] E)
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 = 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 ↔ 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) :
‖(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)

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

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 ⇑(adjoint A)
source
theorem ContinuousLinearMap.adjoint_innerSL_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (x : E) :
adjoint ((innerSL 𝕜) x) = toSpanSingleton 𝕜 x
source
theorem ContinuousLinearMap.adjoint_toSpanSingleton {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (x : E) :
adjoint (toSpanSingleton 𝕜 x) = (innerSL 𝕜) x
source
theorem ContinuousLinearMap.innerSL_apply_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (x : F) (f : E →L[𝕜] F) :
((innerSL 𝕜) x).comp f = (innerSL 𝕜) ((adjoint f) x)
source
theorem ContinuousLinearMap.innerSL_apply_comp_of_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) {f : E →L[𝕜] E} (hf : (↑f).IsSymmetric) :
((innerSL 𝕜) x).comp f = (innerSL 𝕜) (f x)

### 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
@[simp]
theorem isSelfAdjoint_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
IsSelfAdjoint U.starProjection

The orthogonal projection is self-adjoint.

source
@[deprecated isSelfAdjoint_starProjection (since := "2025-07-05")]
theorem orthogonalProjection_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
IsSelfAdjoint U.starProjection

Alias of `isSelfAdjoint_starProjection`.

The orthogonal projection is self-adjoint.

source
theorem IsSelfAdjoint.conj_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] :
IsSelfAdjoint (U.starProjection.comp (T.comp U.starProjection))
source
@[deprecated IsSelfAdjoint.conj_starProjection (since := "2025-07-05")]
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) [U.HasOrthogonalProjection] :
IsSelfAdjoint (U.starProjection.comp (T.comp U.starProjection))

Alias of `IsSelfAdjoint.conj_starProjection`.

source
theorem ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] :
IsStarNormal T ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

An operator `T` is normal iff `‖T v‖ = ‖(adjoint T) v‖` for all `v`.

source
theorem ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] (hT : IsStarNormal T) (x : E) :
(adjoint T) x = 0 ↔ T x = 0
source
theorem ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] (hT : IsStarNormal T) :
LinearMap.ker (adjoint T) = LinearMap.ker T
source
theorem ContinuousLinearMap.IsStarNormal.orthogonal_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] (hT : IsStarNormal T) :
(LinearMap.range T)ᗮ = LinearMap.ker T

The range of a normal operator is pairwise orthogonal to its kernel.

This is a weaker version of `LinearMap.IsSymmetric.orthogonal_range` but with stronger type class assumptions (i.e., `CompleteSpace`).

source
theorem ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] (hT : IsIdempotentElem T) :
IsSelfAdjoint T ↔ IsStarNormal T

An idempotent operator is self-adjoint iff it is normal.

source
theorem ContinuousLinearMap.isStarProjection_iff_isIdempotentElem_and_isStarNormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] :
IsStarProjection T ↔ IsIdempotentElem T ∧ IsStarNormal T

A continuous linear map is a star projection iff it is idempotent and normal.

source
theorem ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] :
IsStarProjection T ↔ (↑T).IsSymmetricProjection
source
theorem ContinuousLinearMap.IsStarProjection.ext_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] {S : E →L[𝕜] E} (hS : IsStarProjection S) (hT : IsStarProjection T) :
S = T ↔ LinearMap.range S = LinearMap.range T

Star projection operators are equal iff their range are.

source
theorem ContinuousLinearMap.IsStarProjection.ext {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] {S : E →L[𝕜] E} (hS : IsStarProjection S) (hT : IsStarProjection T) :
LinearMap.range S = LinearMap.range T → S = T

Alias of the reverse direction of `ContinuousLinearMap.IsStarProjection.ext_iff`.

Star projection operators are equal iff their range are.

source
@[simp]
theorem isStarProjection_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] :
IsStarProjection U.starProjection

`U.starProjection` is a star projection.

source
theorem isStarProjection_iff_eq_starProjection_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} :
IsStarProjection p ↔ ∃ (x : (LinearMap.range p).HasOrthogonalProjection), p = (LinearMap.range p).starProjection

An operator is a star projection if and only if it is an orthogonal projection.

source
theorem isStarProjection_iff_eq_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} :
IsStarProjection p ↔ ∃ (K : Submodule 𝕜 E) (x : K.HasOrthogonalProjection), p = K.starProjection
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 = (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) :
toContinuousLinearMap (adjoint A) = ContinuousLinearMap.adjoint (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) :
adjoint A = ↑(ContinuousLinearMap.adjoint (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) :
inner 𝕜 ((adjoint A) y) x = inner 𝕜 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) :
inner 𝕜 x ((adjoint A) y) = inner 𝕜 (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) :
adjoint (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) :
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.

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 = 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`.

source
@[simp]
theorem LinearMap.IsSymmetric.adjoint_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hA : A.IsSymmetric) :
adjoint A = A
source
theorem LinearMap.adjoint_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
adjoint id = id
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₁ : Module.Basis ι₁ 𝕜 E) (b₂ : Module.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`.

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 : Module.Basis ι 𝕜 E) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = adjoint B ↔ ∀ (i : ι) (y : F), inner 𝕜 (A (b i)) y = inner 𝕜 (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 : Module.Basis ι 𝕜 F) (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) :
A = adjoint B ↔ ∀ (i : ι) (x : E), inner 𝕜 (A x) (b i) = inner 𝕜 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 = { toStar := LinearMap.instStarId, star_involutive := ⋯ }

source
instance LinearMap.instStarMulId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
StarMul (E →ₗ[𝕜] E)
Equations

- LinearMap.instStarMulId = { toInvolutiveStar := LinearMap.instInvolutiveStarId, star_mul := ⋯ }

source
instance LinearMap.instStarRingId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
StarRing (E →ₗ[𝕜] E)
Equations

- LinearMap.instStarRingId = { toStarMul := LinearMap.instStarMulId, star_add := ⋯ }

source
instance LinearMap.instStarModuleId {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
StarModule 𝕜 (E →ₗ[𝕜] E)
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 = 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 ↔ 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 ⇑(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) :
(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 (inner 𝕜 x ((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 (inner 𝕜 x ((adjoint T) (T x))) = 0
source
theorem LinearMap.isSelfAdjoint_toContinuousLinearMap_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) :
have this := ⋯; IsSelfAdjoint (toContinuousLinearMap T) ↔ IsSelfAdjoint T
source
theorem ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →L[𝕜] E) :
have this := ⋯; IsSelfAdjoint ↑T ↔ IsSelfAdjoint T
source
theorem LinearMap.isStarProjection_toContinuousLinearMap_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} :
have this := ⋯; IsStarProjection (toContinuousLinearMap T) ↔ IsStarProjection T
source
theorem LinearMap.isStarProjection_iff_isSymmetricProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} :
IsStarProjection T ↔ T.IsSymmetricProjection
source
theorem LinearMap.IsStarProjection.ext_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {S T : E →ₗ[𝕜] E} (hS : IsStarProjection S) (hT : IsStarProjection T) :
S = T ↔ range S = range T

Star projection operators are equal iff their range are.

source
theorem LinearMap.IsStarProjection.ext {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {S T : E →ₗ[𝕜] E} (hS : IsStarProjection S) (hT : IsStarProjection T) :
range S = range T → S = T

Alias of the reverse direction of `LinearMap.IsStarProjection.ext_iff`.

Star projection operators are equal iff their range are.

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), inner 𝕜 (u x) (u y) = inner 𝕜 x y) ↔ (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‖) ↔ (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 y : H) :
inner 𝕜 (u x) (u y) = inner 𝕜 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 y : H) :
inner 𝕜 (↑u x) (↑u y) = inner 𝕜 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 := (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) :
↑(linearIsometryEquiv.symm e) = ↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
source
@[deprecated Unitary.norm_map (since := "2025-10-29")]
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‖

Alias of `Unitary.norm_map`.

source
@[deprecated Unitary.inner_map_map (since := "2025-10-29")]
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

Alias of `Unitary.inner_map_map`.

source
@[deprecated Unitary.linearIsometryEquiv (since := "2025-10-29")]
def unitary.linearIsometryEquiv {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] :
↥(unitary (H →L[𝕜] H)) ≃* (H ≃ₗᵢ[𝕜] H)

Alias of `Unitary.linearIsometryEquiv`.

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

Equations

- @unitary.linearIsometryEquiv = @Unitary.linearIsometryEquiv

Instances For

source
@[deprecated Unitary.linearIsometryEquiv_coe_apply (since := "2025-10-29")]
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

Alias of `Unitary.linearIsometryEquiv_coe_apply`.

source
@[deprecated Unitary.linearIsometryEquiv_coe_symm_apply (since := "2025-10-29")]
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 := ⋯ }

Alias of `Unitary.linearIsometryEquiv_coe_symm_apply`.

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 𝕜) :
(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.

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) :
(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.

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