Symmetric linear maps in an inner product space #

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

This file defines and proves basic theorems about symmetric not necessarily bounded operators on an inner product space, i.e linear maps T : E → E such that ∀ x y, ⟪T x, y⟫ = ⟪x, T y⟫.

In comparison to is_self_adjoint, this definition works for non-continuous linear maps, and doesn't rely on the definition of the adjoint, which allows it to be stated in non-complete space.

Main definitions #

linear_map.is_symmetric: a (not necessarily bounded) operator on an inner product space is symmetric, if for all x, y, we have ⟪T x, y⟫ = ⟪x, T y⟫

Main statements #

is_symmetric.continuous: if a symmetric operator is defined on a complete space, then it is automatically continuous.

Tags #

self-adjoint, symmetric

Symmetric operators #

source

def linear_map.is_symmetric {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (T : E →ₗ[𝕜] E) :

Prop

A (not necessarily bounded) operator on an inner product space is symmetric, if for all x, y, we have ⟪T x, y⟫ = ⟪x, T y⟫.

Equations

T.is_symmetric = ∀ (x y : E), has_inner.inner (⇑T x) y = has_inner.inner x (⇑T y)

source

theorem linear_map.is_symmetric_iff_sesq_form {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] (T : E →ₗ[𝕜] E) :

T.is_symmetric ↔ sesq_form_of_inner.is_self_adjoint T

An operator T on an inner product space is symmetric if and only if it is linear_map.is_self_adjoint with respect to the sesquilinear form given by the inner product.

source

theorem linear_map.is_symmetric.conj_inner_sym {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) (x y : E) :

⇑(star_ring_end 𝕜) (has_inner.inner (⇑T x) y) = has_inner.inner (⇑T y) x

source

@[simp]

theorem linear_map.is_symmetric.apply_clm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →L[𝕜] E} (hT : ↑T.is_symmetric) (x y : E) :

has_inner.inner (⇑T x) y = has_inner.inner x (⇑T y)

source

theorem linear_map.is_symmetric_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] :

0.is_symmetric

source

theorem linear_map.is_symmetric_id {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] :

linear_map.id.is_symmetric

source

theorem linear_map.is_symmetric.add {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {T S : E →ₗ[𝕜] E} (hT : T.is_symmetric) (hS : S.is_symmetric) :

(T + S).is_symmetric

source

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

continuous ⇑T

The Hellinger--Toeplitz theorem: if a symmetric operator is defined on a complete space, then it is automatically continuous.

source

@[simp]

theorem linear_map.is_symmetric.coe_re_apply_inner_self_apply {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →L[𝕜] E} (hT : ↑T.is_symmetric) (x : E) :

↑(T.re_apply_inner_self x) = has_inner.inner (⇑T x) x

For a symmetric operator T, the function λ x, ⟪T x, x⟫ is real-valued.

source

theorem linear_map.is_symmetric.restrict_invariant {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) {V : submodule 𝕜 E} (hV : ∀ (v : E), v ∈ V → ⇑T v ∈ V) :

(T.restrict hV).is_symmetric

If a symmetric operator preserves a submodule, its restriction to that submodule is symmetric.

source

theorem linear_map.is_symmetric.restrict_scalars {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) :

(linear_map.restrict_scalars ℝ T).is_symmetric

source

theorem linear_map.is_symmetric_iff_inner_map_self_real {V : Type u_6} [normed_add_comm_group V] [inner_product_space ℂ V] (T : V →ₗ[ℂ ] V) :

T.is_symmetric ↔ ∀ (v : V), ⇑(star_ring_end ℂ) (has_inner.inner (⇑T v) v) = has_inner.inner (⇑T v) v

A linear operator on a complex inner product space is symmetric precisely when ⟪T v, v⟫_ℂ is real for all v.

source

theorem linear_map.is_symmetric.inner_map_polarization {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) (x y : E) :

has_inner.inner (⇑T x) y = (has_inner.inner (⇑T (x + y)) (x + y) - has_inner.inner (⇑T (x - y)) (x - y) - is_R_or_C.I * has_inner.inner (⇑T (x + is_R_or_C.I • y)) (x + is_R_or_C.I • y) + is_R_or_C.I * has_inner.inner (⇑T (x - is_R_or_C.I • y)) (x - is_R_or_C.I • y)) / 4

Polarization identity for symmetric linear maps. See inner_map_polarization for the complex version without the symmetric assumption.

source

theorem linear_map.is_symmetric.inner_map_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) :

(∀ (x : E), has_inner.inner (⇑T x) x = 0) ↔ T = 0

A symmetric linear map T is zero if and only if ⟪T x, x⟫_ℝ = 0 for all x. See inner_map_self_eq_zero for the complex version without the symmetric assumption.