mathlib3 documentation

analysis.inner_product_space.adjoint

Adjoint of operators on Hilbert spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Implementation notes #

Tags #

adjoint

Adjoint operator #

noncomputable def continuous_linear_map.adjoint_aux {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [complete_space 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
noncomputable def continuous_linear_map.adjoint {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [complete_space E] [complete_space F] :
(E β†’L[π•œ] F) ≃ₗᡒ⋆[π•œ] F β†’L[π•œ] E

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

Equations

The fundamental property of the adjoint.

The fundamental property of the adjoint.

@[simp]

The adjoint is involutive

@[simp]

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

theorem continuous_linear_map.eq_adjoint_iff {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [complete_space E] [complete_space F] (A : E β†’L[π•œ] F) (B : F β†’L[π•œ] E) :

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.

@[protected, instance]
noncomputable def continuous_linear_map.has_star {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] :
has_star (E β†’L[π•œ] E)

E β†’L[π•œ] E is a star algebra with the adjoint as the star operation.

Equations
@[protected, instance]
noncomputable def continuous_linear_map.star_ring {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] :
star_ring (E β†’L[π•œ] E)
Equations
@[protected, instance]
def continuous_linear_map.star_module {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] :
star_module π•œ (E β†’L[π•œ] E)

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

@[protected, instance]
def continuous_linear_map.cstar_ring {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] :
cstar_ring (E β†’L[π•œ] E)

Self-adjoint operators #

theorem is_self_adjoint.adjoint_eq {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] {A : E β†’L[π•œ] E} (hA : is_self_adjoint A) :
theorem is_self_adjoint.is_symmetric {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] {A : E β†’L[π•œ] E} (hA : is_self_adjoint A) :

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

theorem is_self_adjoint.conj_adjoint {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [complete_space E] [complete_space F] {T : E β†’L[π•œ] E} (hT : is_self_adjoint T) (S : E β†’L[π•œ] F) :

Conjugating preserves self-adjointness

theorem is_self_adjoint.adjoint_conj {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [complete_space E] [complete_space F] {T : E β†’L[π•œ] E} (hT : is_self_adjoint T) (S : F β†’L[π•œ] E) :

Conjugating preserves self-adjointness

theorem linear_map.is_symmetric.is_self_adjoint {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] {A : E β†’L[π•œ] E} (hA : ↑A.is_symmetric) :

The orthogonal projection is self-adjoint.

def linear_map.is_symmetric.to_self_adjoint {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] {T : E β†’β‚—[π•œ] E} (hT : T.is_symmetric) :

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

Equations
theorem linear_map.is_symmetric.coe_to_self_adjoint {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] {T : E β†’β‚—[π•œ] E} (hT : T.is_symmetric) :
theorem linear_map.is_symmetric.to_self_adjoint_apply {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [complete_space E] {T : E β†’β‚—[π•œ] E} (hT : T.is_symmetric) {x : E} :
noncomputable def linear_map.adjoint {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [finite_dimensional π•œ E] [finite_dimensional π•œ 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
theorem linear_map.adjoint_inner_left {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [finite_dimensional π•œ E] [finite_dimensional π•œ F] (A : E β†’β‚—[π•œ] F) (x : E) (y : F) :

The fundamental property of the adjoint.

theorem linear_map.adjoint_inner_right {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [finite_dimensional π•œ E] [finite_dimensional π•œ F] (A : E β†’β‚—[π•œ] F) (x : E) (y : F) :

The fundamental property of the adjoint.

@[simp]
theorem linear_map.adjoint_adjoint {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [finite_dimensional π•œ E] [finite_dimensional π•œ F] (A : E β†’β‚—[π•œ] F) :

The adjoint is involutive

@[simp]
theorem linear_map.adjoint_comp {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [normed_add_comm_group G] [inner_product_space π•œ E] [inner_product_space π•œ F] [inner_product_space π•œ G] [finite_dimensional π•œ E] [finite_dimensional π•œ F] [finite_dimensional π•œ G] (A : F β†’β‚—[π•œ] G) (B : E β†’β‚—[π•œ] F) :

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

theorem linear_map.eq_adjoint_iff {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [finite_dimensional π•œ E] [finite_dimensional π•œ F] (A : E β†’β‚—[π•œ] F) (B : F β†’β‚—[π•œ] E) :

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

theorem linear_map.eq_adjoint_iff_basis {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [finite_dimensional π•œ E] [finite_dimensional π•œ F] {ι₁ : Type u_4} {ΞΉβ‚‚ : Type u_5} (b₁ : basis ι₁ π•œ E) (bβ‚‚ : basis ΞΉβ‚‚ π•œ F) (A : E β†’β‚—[π•œ] F) (B : F β†’β‚—[π•œ] E) :
A = ⇑linear_map.adjoint B ↔ βˆ€ (i₁ : ι₁) (iβ‚‚ : ΞΉβ‚‚), has_inner.inner (⇑A (⇑b₁ i₁)) (⇑bβ‚‚ iβ‚‚) = has_inner.inner (⇑b₁ i₁) (⇑B (⇑bβ‚‚ iβ‚‚))

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

theorem linear_map.eq_adjoint_iff_basis_left {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [finite_dimensional π•œ E] [finite_dimensional π•œ F] {ΞΉ : Type u_4} (b : basis ΞΉ π•œ E) (A : E β†’β‚—[π•œ] F) (B : F β†’β‚—[π•œ] E) :
theorem linear_map.eq_adjoint_iff_basis_right {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C π•œ] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space π•œ E] [inner_product_space π•œ F] [finite_dimensional π•œ E] [finite_dimensional π•œ F] {ΞΉ : Type u_4} (b : basis ΞΉ π•œ F) (A : E β†’β‚—[π•œ] F) (B : F β†’β‚—[π•œ] E) :
@[protected, instance]
noncomputable def linear_map.has_star {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] :
has_star (E β†’β‚—[π•œ] E)

E β†’β‚—[π•œ] E is a star algebra with the adjoint as the star operation.

Equations
@[protected, instance]
noncomputable def linear_map.has_involutive_star {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] :
Equations
@[protected, instance]
noncomputable def linear_map.star_semigroup {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] :
Equations
@[protected, instance]
noncomputable def linear_map.star_ring {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] :
Equations
@[protected, instance]
def linear_map.star_module {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] :
star_module π•œ (E β†’β‚—[π•œ] E)
theorem linear_map.star_eq_adjoint {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] (A : E β†’β‚—[π•œ] E) :
theorem linear_map.is_self_adjoint_iff' {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] {A : E β†’β‚—[π•œ] E} :

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

theorem linear_map.is_symmetric_iff_is_self_adjoint {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] (A : E β†’β‚—[π•œ] E) :
theorem linear_map.is_symmetric_adjoint_mul_self {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] (T : E β†’β‚—[π•œ] E) :

The Gram operator T†T is symmetric.

The Gram operator T†T is a positive operator.

@[simp]
theorem linear_map.im_inner_adjoint_mul_self_eq_zero {π•œ : Type u_1} {E : Type u_2} [is_R_or_C π•œ] [normed_add_comm_group E] [inner_product_space π•œ E] [finite_dimensional π•œ E] (T : E β†’β‚—[π•œ] E) (x : E) :

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