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.

References #

Sheldon Axler, Linear Algebra Done Right

Tags #

adjoint

Adjoint operator #

source

noncomputable 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 ∘SL B) = adjoint B ∘SL 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 ∘SL 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 ∘SL 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 ∘SL 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 ∘SL 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 ContinuousLinearMap.adjoint_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

adjoint 1 = 1

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

(↑T).kerᗮ = (↑(adjoint T)).range.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) :

(↑T).rangeᗮ = (↑(adjoint T)).ker

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

(↑U).ker ≤ (↑T).ker ↔ (↑T).range ≤ (↑U).range

source

theorem ContinuousLinearMap.ker_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] (T : E →L[𝕜] F) :

(↑(adjoint T ∘SL T)).ker = (↑T).ker

Infinite-dimensional version of 7.64(b) in [Axl24].

source

theorem ContinuousLinearMap.ker_self_comp_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[𝕜] F) :

(↑(T ∘SL adjoint T)).ker = (↑(adjoint T)).ker

source

theorem ContinuousLinearMap.adjoint_comp_self_injective_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] (T : E →L[𝕜] F) :

Function.Injective (⇑(adjoint T) ∘ ⇑T) ↔ Function.Injective ⇑T

This lemma uses the simp-normal form ⇑(T†) ∘ ⇑T instead of ⇑(T† ∘L T) (note the difference between ∘ and ∘L). You may need to rewrite with ContinuousLinearMap.coe_comp' before applying this lemma.

source

theorem ContinuousLinearMap.self_comp_adjoint_injective_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] (T : E →L[𝕜] F) :

Function.Injective (⇑T ∘ ⇑(adjoint T)) ↔ Function.Injective ⇑(adjoint T)

This lemma uses the simp-normal form ⇑T ∘ ⇑(T†) instead of ⇑(T ∘L T†) (note the difference between ∘ and ∘L). You may need to rewrite with ContinuousLinearMap.coe_comp' before applying this lemma.

source

@[implicit_reducible]

noncomputable 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

@[implicit_reducible]

noncomputable 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

@[implicit_reducible]

noncomputable 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

@[implicit_reducible]

noncomputable 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

@[simp]

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

ContinuousLinearMap.id 𝕜 E ∈ unitary (E →L[𝕜] E)

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 ∘SL A‖ = ‖A‖ * ‖A‖

source

@[simp]

theorem ContinuousLinearMap.adjoint_comp_self_eq_zero_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} :

adjoint A ∘SL A = 0 ↔ A = 0

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

(innerₛₗ 𝕜).flip.IsAdjointPair (innerₛₗ 𝕜).flip ⇑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 ∘SL 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 ∘SL f = (innerSL 𝕜) (f x)

source

@[simp]

theorem InnerProductSpace.adjoint_rankOne {𝕜 : 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 : E) (y : F) :

ContinuousLinearMap.adjoint (((rankOne 𝕜) x) y) = ((rankOne 𝕜) y) x

source

theorem InnerProductSpace.rankOne_comp {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {E : Type u_5} {G : Type u_6} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] (x : E) (y : F) (f : G →L[𝕜] F) :

((rankOne 𝕜) x) y ∘SL f = ((rankOne 𝕜) x) ((ContinuousLinearMap.adjoint f) y)

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 ∘SL T ∘SL 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 ∘SL T ∘SL 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

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 ∘SL T ∘SL U.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) :

(↑(adjoint T)).ker = (↑T).ker

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

(↑T).rangeᗮ = (↑T).ker

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.isSymmetricProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] :

IsStarProjection T → (↑T).IsSymmetricProjection

Alias of the forward direction of ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection.

source

theorem ContinuousLinearMap.LinearMap.IsSymmetricProjection.isStarProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} [CompleteSpace E] :

(↑T).IsSymmetricProjection → IsStarProjection T

Alias of the reverse direction of ContinuousLinearMap.isStarProjection_iff_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 ↔ (↑S).range = (↑T).range

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

(↑S).range = (↑T).range → S = T

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

Star projection operators are equal iff their range are.

source

theorem InnerProductSpace.isStarProjection_rankOne_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {x : E} (hx : ‖x‖ = 1) :

IsStarProjection (((rankOne 𝕜) x) x)

source

theorem ContinuousLinearMap.orthogonal_mem_invtSubmodule {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} {U : Submodule 𝕜 E} (h : U ∈ Module.End.invtSubmodule ↑(adjoint T)) :

Uᗮ ∈ Module.End.invtSubmodule ↑T

source

theorem ContinuousLinearMap.mem_invtSubmodule_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] :

U ∈ Module.End.invtSubmodule ↑(adjoint T) ↔ Uᗮ ∈ Module.End.invtSubmodule ↑T

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 : (↑p).range.HasOrthogonalProjection), p = (↑p).range.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

noncomputable 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 ContinuousLinearMap.adjoint_toLinearMap {𝕜 : 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 →L[𝕜] F) :

LinearMap.adjoint ↑A = ↑(adjoint 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.adjoint_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

adjoint 1 = 1

source

theorem LinearMap.orthogonal_ker {𝕜 : 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) :

A.kerᗮ = (adjoint A).range

7.6(b) from [Axl24]. See ContinuousLinearMap.orthogonal_ker for the infinite-dimensional version.

source

theorem LinearMap.orthogonal_range {𝕜 : 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) :

A.rangeᗮ = (adjoint A).ker

7.6(a) from [Axl24]. See ContinuousLinearMap.orthogonal_range for the infinite-dimensional version.

source

theorem LinearMap.ker_adjoint_comp_self {𝕜 : 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 ∘ₗ A).ker = A.ker

7.64(b) in [Axl24]

source

theorem LinearMap.ker_self_comp_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) :

(A ∘ₗ adjoint A).ker = (adjoint A).ker

source

theorem LinearMap.adjoint_comp_self_injective_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) :

Function.Injective (⇑(adjoint A) ∘ ⇑A) ↔ Function.Injective ⇑A

This lemma uses the simp-normal form ⇑(A.adjoint) ∘ ⇑A instead of ⇑(A.adjoint ∘ₗ A) (note the difference between ∘ and ∘ₗ). You may need to rewrite with LinearMap.coe_comp before applying this lemma.

source

theorem LinearMap.self_comp_adjoint_injective_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) :

Function.Injective (⇑A ∘ ⇑(adjoint A)) ↔ Function.Injective ⇑(adjoint A)

This lemma uses the simp-normal form ⇑A ∘ ⇑(A.adjoint) instead of ⇑(A ∘ₗ A.adjoint) (note the difference between ∘ and ∘ₗ). You may need to rewrite with LinearMap.coe_comp before applying this lemma.

source

theorem LinearMap.range_adjoint_comp_self {𝕜 : 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 ∘ₗ A).range = (adjoint A).range

7.64(c) in [Axl24].

source

theorem LinearMap.range_self_comp_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) :

(A ∘ₗ adjoint A).range = A.range

source

theorem LinearMap.finrank_range_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) :

Module.finrank 𝕜 ↥(adjoint A).range = Module.finrank 𝕜 ↥A.range

Part of 7.64(d) in [Axl24].

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

@[implicit_reducible]

noncomputable 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

@[implicit_reducible]

noncomputable 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

@[implicit_reducible]

noncomputable 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

@[implicit_reducible]

noncomputable 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

@[simp]

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

id ∈ unitary (E →ₗ[𝕜] E)

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

(innerₛₗ 𝕜).flip.IsAdjointPair (innerₛₗ 𝕜).flip ⇑A ⇑(adjoint A)

This next batch of lemmas is based on theorems like LinearMap.IsPositive.conj_adjoint, which are in a downstream file but historically existed before these lemmas. We can't put them in the file where LinearMap.IsSymmetric is defined because they depend on the adjoint.

source

theorem LinearMap.IsSymmetric.conj_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] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (S : E →ₗ[𝕜] F) :

(S ∘ₗ T ∘ₗ adjoint S).IsSymmetric

source

theorem LinearMap.isSymmetric_self_comp_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] (T : E →ₗ[𝕜] F) :

(T ∘ₗ adjoint T).IsSymmetric

source

theorem LinearMap.IsSymmetric.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (S : F →ₗ[𝕜] E) :

(adjoint S ∘ₗ T ∘ₗ S).IsSymmetric

source

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

(adjoint T ∘ₗ T).IsSymmetric

Like LinearMap.isSymmetric_adjoint_mul_self but domain and range can be different

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. See LinearMap.isSymmetric_adjoint_comp_self for a version where the domain and codomain are distinct.

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 ↔ S.range = T.range

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

S.range = T.range → S = T

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

Star projection operators are equal iff their range are.

source

theorem LinearMap.adjoint_innerₛₗ_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (x : E) :

adjoint ((innerₛₗ 𝕜) x) = toSpanSingleton 𝕜 E x

source

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

adjoint (toSpanSingleton 𝕜 E x) = (innerₛₗ 𝕜) x

source

theorem Module.End.mem_invtSubmodule_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {U : Submodule 𝕜 E} :

U ∈ invtSubmodule (LinearMap.adjoint T) ↔ Uᗮ ∈ invtSubmodule T

The linear map version of ContinuousLinearMap.mem_invtSubmodule_adjoint_iff in a finite-dimensional space.

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 ∘SL 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 ∘SL u = 1

source

theorem ContinuousLinearMap.isometry_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) :

Isometry ⇑u ↔ adjoint u ∘SL 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 ↑↑e = ↑↑e.symm

source

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

LinearMap.adjoint ↑e.toLinearEquiv = ↑e.symm.toLinearEquiv

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 ↑↑e = ↑↑e.symm

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

noncomputable def LinearIsometryEquiv.conjStarAlgEquiv {𝕜 : 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) :

(H →L[𝕜] H) ≃⋆ₐ[𝕜] K →L[𝕜] K

An isometric linear equivalence of two Hilbert spaces induces an equivalence of ⋆-algebras of their endomorphisms.

When H = K, this is exactly Unitary.conjStarAlgAut (see Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv and Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv).

Equations

e.conjStarAlgEquiv = StarAlgEquiv.ofAlgEquiv (↑e).conjContinuousAlgEquiv.toAlgEquiv ⋯

Instances For

source

@[simp]

theorem LinearIsometryEquiv.conjStarAlgEquiv_apply_apply {𝕜 : 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) (x : H →L[𝕜] H) (y : K) :

(e.conjStarAlgEquiv x) y = e (x (e.symm y))

source

theorem LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply {𝕜 : 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) (f : K →L[𝕜] K) (x : H) :

(e.conjStarAlgEquiv.symm f) x = e.symm (f (e x))

source

theorem LinearIsometryEquiv.conjStarAlgEquiv_apply {𝕜 : 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) (x : H →L[𝕜] H) :

e.conjStarAlgEquiv x = ↑↑e ∘SL x ∘SL ↑↑e.symm

source

@[simp]

theorem LinearIsometryEquiv.symm_conjStarAlgEquiv {𝕜 : 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) :

e.conjStarAlgEquiv.symm = e.symm.conjStarAlgEquiv

source

@[simp]

theorem LinearIsometryEquiv.conjStarAlgEquiv_refl {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] :

(refl 𝕜 H).conjStarAlgEquiv = StarAlgEquiv.refl

source

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

(e.trans f).conjStarAlgEquiv = e.conjStarAlgEquiv.trans f.conjStarAlgEquiv

source

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

f.conjStarAlgEquiv = g.conjStarAlgEquiv ↔ ∃ (α : ↥(unitary 𝕜)), f = α • g

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.coe_linearIsometryEquiv_apply {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (u : ↥(unitary (H →L[𝕜] H))) :

↑↑(linearIsometryEquiv u) = ↑u

source

@[deprecated Unitary.coe_linearIsometryEquiv_apply (since := "2025-12-16")]

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

↑↑(linearIsometryEquiv u) = ↑u

Alias of Unitary.coe_linearIsometryEquiv_apply.

source

@[simp]

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

↑(linearIsometryEquiv.symm e) = ↑↑e

source

@[deprecated Unitary.coe_symm_linearIsometryEquiv_apply (since := "2025-12-16")]

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) = ↑↑e

Alias of Unitary.coe_symm_linearIsometryEquiv_apply.

source

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

(linearIsometryEquiv u).conjStarAlgEquiv = (conjStarAlgAut 𝕜 (H →L[𝕜] H)) u

source

theorem Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_5} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H] (u : H ≃ₗᵢ[𝕜] H) :

(conjStarAlgAut 𝕜 (H →L[𝕜] H)) (linearIsometryEquiv.symm u) = u.conjStarAlgEquiv

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

noncomputable 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.

source

@[simp]

theorem LinearIsometry.adjoint_comp_self {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_5} {E' : Type u_6} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [CompleteSpace E'] (f : E →ₗᵢ[𝕜] E') :

ContinuousLinearMap.adjoint f.toContinuousLinearMap ∘SL f.toContinuousLinearMap = 1

source

@[simp]

theorem LinearIsometry.adjoint_comp_self' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_5} {E' : Type u_6} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] [FiniteDimensional 𝕜 E'] (f : E →ₗᵢ[𝕜] E') :

LinearMap.adjoint f.toLinearMap ∘ₗ f.toLinearMap = LinearMap.id

A version of LinearIsometry.adjoint_comp_self in terms of LinearMap.adjoint.

source

theorem LinearIsometryEquiv.toMatrix_mem_unitaryGroup {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_5} {E : Type u_6} {E' : Type u_7} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (b : OrthonormalBasis ι 𝕜 E) (b' : OrthonormalBasis ι 𝕜 E') :

(LinearMap.toMatrix b.toBasis b'.toBasis) ↑f.toLinearEquiv ∈ Matrix.unitaryGroup ι 𝕜

Documentation

Mathlib.Analysis.InnerProductSpace.Adjoint

Adjoint of operators on Hilbert spaces #

Main definitions #

Implementation notes #

References #

Tags #

Adjoint operator #

Self-adjoint operators #