analysis.inner_product_space.adjoint

source

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

continuous_linear_map.adjoint_aux = (⇑(continuous_linear_map.compSL F (normed_space.dual 𝕜 E) E (star_ring_end 𝕜) (star_ring_end 𝕜)) ↑((inner_product_space.to_dual 𝕜 E).symm)).comp continuous_linear_map.to_sesq_form

source

@[simp]

theorem continuous_linear_map.adjoint_aux_apply {𝕜 : 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] (A : E →L[𝕜] F) (x : F) :

⇑(⇑continuous_linear_map.adjoint_aux A) x = ⇑((inner_product_space.to_dual 𝕜 E).symm) (⇑(⇑continuous_linear_map.to_sesq_form A) x)

source

theorem continuous_linear_map.adjoint_aux_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] [complete_space E] (A : E →L[𝕜] F) (x : E) (y : F) :

has_inner.inner (⇑(⇑continuous_linear_map.adjoint_aux A) y) x = has_inner.inner y (⇑A x)

source

theorem continuous_linear_map.adjoint_aux_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] [complete_space E] (A : E →L[𝕜] F) (x : E) (y : F) :

has_inner.inner x (⇑(⇑continuous_linear_map.adjoint_aux A) y) = has_inner.inner (⇑A x) y

source

theorem continuous_linear_map.adjoint_aux_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] [complete_space F] (A : E →L[𝕜] F) :

⇑continuous_linear_map.adjoint_aux (⇑continuous_linear_map.adjoint_aux A) = A

source

@[simp]

theorem continuous_linear_map.adjoint_aux_norm {𝕜 : 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) :

‖⇑continuous_linear_map.adjoint_aux A‖ = ‖A‖

source

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

continuous_linear_map.adjoint = linear_isometry_equiv.of_surjective {to_linear_map := continuous_linear_map.adjoint_aux.to_linear_map, norm_map' := _} continuous_linear_map.adjoint._proof_21

source

theorem continuous_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] [complete_space E] [complete_space F] (A : E →L[𝕜] F) (x : E) (y : F) :

has_inner.inner (⇑(⇑continuous_linear_map.adjoint A) y) x = has_inner.inner y (⇑A x)

The fundamental property of the adjoint.

source

theorem continuous_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] [complete_space E] [complete_space F] (A : E →L[𝕜] F) (x : E) (y : F) :

has_inner.inner x (⇑(⇑continuous_linear_map.adjoint A) y) = has_inner.inner (⇑A x) y

The fundamental property of the adjoint.

source

@[simp]

theorem continuous_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] [complete_space E] [complete_space F] (A : E →L[𝕜] F) :

⇑continuous_linear_map.adjoint (⇑continuous_linear_map.adjoint A) = A

The adjoint is involutive

source

@[simp]

theorem continuous_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] [complete_space E] [complete_space G] [complete_space F] (A : F →L[𝕜] G) (B : E →L[𝕜] F) :

⇑continuous_linear_map.adjoint (A.comp B) = (⇑continuous_linear_map.adjoint B).comp (⇑continuous_linear_map.adjoint A)

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

source

theorem continuous_linear_map.apply_norm_sq_eq_inner_adjoint_left {𝕜 : 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) (x : E) :

‖⇑A x‖ ^ 2 = ⇑is_R_or_C.re (has_inner.inner (⇑(⇑continuous_linear_map.adjoint A * A) x) x)

source

theorem continuous_linear_map.apply_norm_eq_sqrt_inner_adjoint_left {𝕜 : 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) (x : E) :

‖⇑A x‖ = √ (⇑is_R_or_C.re (has_inner.inner (⇑(⇑continuous_linear_map.adjoint A * A) x) x))

source

theorem continuous_linear_map.apply_norm_sq_eq_inner_adjoint_right {𝕜 : 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) (x : E) :

‖⇑A x‖ ^ 2 = ⇑is_R_or_C.re (has_inner.inner x (⇑(⇑continuous_linear_map.adjoint A * A) x))

source

theorem continuous_linear_map.apply_norm_eq_sqrt_inner_adjoint_right {𝕜 : 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) (x : E) :

‖⇑A x‖ = √ (⇑is_R_or_C.re (has_inner.inner x (⇑(⇑continuous_linear_map.adjoint A * A) x)))

source

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

A = ⇑continuous_linear_map.adjoint B ↔ ∀ (x : E) (y : F), has_inner.inner (⇑A x) y = has_inner.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 continuous_linear_map.adjoint_id {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] :

⇑continuous_linear_map.adjoint (continuous_linear_map.id 𝕜 E) = continuous_linear_map.id 𝕜 E

source

theorem submodule.adjoint_subtypeL {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] (U : submodule 𝕜 E) [complete_space ↥U] :

⇑continuous_linear_map.adjoint U.subtypeL = orthogonal_projection U

source

theorem submodule.adjoint_orthogonal_projection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] (U : submodule 𝕜 E) [complete_space ↥U] :

⇑continuous_linear_map.adjoint (orthogonal_projection U) = U.subtypeL

source

@[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

continuous_linear_map.has_star = {star := ⇑continuous_linear_map.adjoint}

source

@[protected, instance]

noncomputable def continuous_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] [complete_space E] :

has_involutive_star (E →L[𝕜] E)

Equations

continuous_linear_map.has_involutive_star = {to_has_star := continuous_linear_map.has_star _inst_8, star_involutive := _}

source

@[protected, instance]

noncomputable def continuous_linear_map.star_semigroup {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] :

star_semigroup (E →L[𝕜] E)

Equations

continuous_linear_map.star_semigroup = {to_has_involutive_star := continuous_linear_map.has_involutive_star _inst_8, star_mul := _}

source

@[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

continuous_linear_map.star_ring = {to_star_semigroup := continuous_linear_map.star_semigroup _inst_8, star_add := _}

source

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

source

theorem continuous_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] [complete_space E] (A : E →L[𝕜] E) :

has_star.star A = ⇑continuous_linear_map.adjoint A

source

theorem continuous_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] [complete_space E] {A : E →L[𝕜] E} :

is_self_adjoint A ↔ ⇑continuous_linear_map.adjoint A = A

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

source

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

source

theorem continuous_linear_map.is_adjoint_pair_inner {E' : Type u_5} {F' : Type u_6} [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') :

sesq_form_of_inner.is_adjoint_pair sesq_form_of_inner ↑A ↑(⇑continuous_linear_map.adjoint A)

source

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

⇑continuous_linear_map.adjoint A = A

source

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

↑A.is_symmetric

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

source

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

is_self_adjoint (S.comp (T.comp (⇑continuous_linear_map.adjoint S)))

Conjugating preserves self-adjointness

source

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

is_self_adjoint ((⇑continuous_linear_map.adjoint S).comp (T.comp S))

Conjugating preserves self-adjointness

source

theorem continuous_linear_map.is_self_adjoint_iff_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} :

is_self_adjoint A ↔ ↑A.is_symmetric

source

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

is_self_adjoint A

source

theorem orthogonal_projection_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] (U : submodule 𝕜 E) [complete_space ↥U] :

is_self_adjoint (U.subtypeL.comp (orthogonal_projection U))

The orthogonal projection is self-adjoint.

source

theorem is_self_adjoint.conj_orthogonal_projection {𝕜 : 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 →L[𝕜] E} (hT : is_self_adjoint T) (U : submodule 𝕜 E) [complete_space ↥U] :

is_self_adjoint (U.subtypeL.comp ((orthogonal_projection U).comp (T.comp (U.subtypeL.comp (orthogonal_projection U)))))

source

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

↥(self_adjoint (E →L[𝕜] E))

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

Equations

hT.to_self_adjoint = ⟨{to_linear_map := T, cont := _}, _⟩

source

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

↑(hT.to_self_adjoint) = T

source

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

⇑(hT.to_self_adjoint) x = ⇑T x

source

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

linear_map.adjoint = (linear_map.to_continuous_linear_map.trans continuous_linear_map.adjoint.to_linear_equiv).trans linear_map.to_continuous_linear_map.symm

source

theorem linear_map.adjoint_to_continuous_linear_map {𝕜 : 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) :

⇑linear_map.to_continuous_linear_map (⇑linear_map.adjoint A) = ⇑continuous_linear_map.adjoint (⇑linear_map.to_continuous_linear_map A)

source

theorem linear_map.adjoint_eq_to_clm_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) :

⇑linear_map.adjoint A = ↑(⇑continuous_linear_map.adjoint (⇑linear_map.to_continuous_linear_map A))

source

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

has_inner.inner (⇑(⇑linear_map.adjoint A) y) x = has_inner.inner y (⇑A x)

The fundamental property of the adjoint.

source

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

has_inner.inner x (⇑(⇑linear_map.adjoint A) y) = has_inner.inner (⇑A x) y

The fundamental property of the adjoint.

source

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

⇑linear_map.adjoint (⇑linear_map.adjoint A) = A

The adjoint is involutive

source

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

⇑linear_map.adjoint (A.comp B) = (⇑linear_map.adjoint B).comp (⇑linear_map.adjoint A)

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

source

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

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

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.

source

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

A = ⇑linear_map.adjoint B ↔ ∀ (i : ι) (y : F), has_inner.inner (⇑A (⇑b i)) y = has_inner.inner (⇑b i) (⇑B y)

source

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

A = ⇑linear_map.adjoint B ↔ ∀ (i : ι) (x : E), has_inner.inner (⇑A x) (⇑b i) = has_inner.inner x (⇑B (⇑b i))

source

@[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

linear_map.has_star = {star := ⇑linear_map.adjoint}

source

@[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] :

has_involutive_star (E →ₗ[𝕜] E)

Equations

linear_map.has_involutive_star = {to_has_star := linear_map.has_star _inst_8, star_involutive := _}

source

@[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] :

star_semigroup (E →ₗ[𝕜] E)

Equations

linear_map.star_semigroup = {to_has_involutive_star := linear_map.has_involutive_star _inst_8, star_mul := _}

source

@[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] :

star_ring (E →ₗ[𝕜] E)

Equations

linear_map.star_ring = {to_star_semigroup := linear_map.star_semigroup _inst_8, star_add := _}

source

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

source

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

has_star.star A = ⇑linear_map.adjoint A

source

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

is_self_adjoint A ↔ ⇑linear_map.adjoint A = A

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

source

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

A.is_symmetric ↔ is_self_adjoint A

source

theorem linear_map.is_adjoint_pair_inner {E' : Type u_5} {F' : Type u_6} [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') :

sesq_form_of_inner.is_adjoint_pair sesq_form_of_inner A (⇑linear_map.adjoint A)

source

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

(⇑linear_map.adjoint T * T).is_symmetric

The Gram operator T†T is symmetric.

source

theorem linear_map.re_inner_adjoint_mul_self_nonneg {𝕜 : 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) :

0 ≤ ⇑is_R_or_C.re (has_inner.inner x (⇑(⇑linear_map.adjoint T * T) x))

The Gram operator T†T is a positive operator.

source

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

⇑is_R_or_C.im (has_inner.inner x (⇑(⇑linear_map.adjoint T) (⇑T x))) = 0

source

theorem matrix.to_euclidean_lin_conj_transpose_eq_adjoint {𝕜 : Type u_1} [is_R_or_C 𝕜] {m : Type u_5} {n : Type u_6} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] (A : matrix m n 𝕜) :

⇑matrix.to_euclidean_lin A.conj_transpose = ⇑linear_map.adjoint (⇑matrix.to_euclidean_lin A)

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

mathlib3 documentation

Adjoint of operators on Hilbert spaces #

Main definitions #

Implementation notes #

Tags #

Adjoint operator #

Self-adjoint operators #