Symmetric linear maps in an inner product space

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 IsSelfAdjoint, 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

• LinearMap.IsSymmetric: 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

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

Tags

self-adjoint, symmetric

Symmetric operators

def LinearMap.IsSymmetric {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 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

• LinearMap.IsSymmetric T = ∀ (x y : E), ⟪T x, y⟫_𝕜 = ⟪x, T y⟫_𝕜

theorem LinearMap.isSymmetric_iff_sesqForm {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) : LinearMap.IsSymmetric T ↔ LinearMap.IsSelfAdjoint sesqFormOfInner T

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

theorem LinearMap.IsSymmetric.conj_inner_sym {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) (x : E) (y : E) : (starRingEnd 𝕜) ⟪T x, y⟫_𝕜 = ⟪T y, x⟫_𝕜

@[simp]

theorem LinearMap.IsSymmetric.apply_clm {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (hT : LinearMap.IsSymmetric ↑T) (x : E) (y : E) : ⟪T x, y⟫_𝕜 = ⟪x, T y⟫_𝕜

theorem LinearMap.isSymmetric_zero {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : LinearMap.IsSymmetric 0

theorem LinearMap.isSymmetric_id {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : LinearMap.IsSymmetric LinearMap.id

theorem LinearMap.IsSymmetric.add {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} {S : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) (hS : LinearMap.IsSymmetric S) : LinearMap.IsSymmetric (T + S)

theorem LinearMap.IsSymmetric.continuous {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) : Continuous ⇑T

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

@[simp]

theorem LinearMap.IsSymmetric.coe_reApplyInnerSelf_apply {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (hT : LinearMap.IsSymmetric ↑T) (x : E) : ↑(ContinuousLinearMap.reApplyInnerSelf T x) = ⟪T x, x⟫_𝕜

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

theorem LinearMap.IsSymmetric.restrict_invariant {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) {V : Submodule 𝕜 E} (hV : ∀ v ∈ V, T v ∈ V) : LinearMap.IsSymmetric (LinearMap.restrict T hV)

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

theorem LinearMap.IsSymmetric.restrictScalars {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) : LinearMap.IsSymmetric (↑ℝ T)

theorem LinearMap.isSymmetric_iff_inner_map_self_real {V : Type u_6} [NormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V) : LinearMap.IsSymmetric T ↔ ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ

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

theorem LinearMap.IsSymmetric.inner_map_polarization {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) (x : E) (y : E) : ⟪T x, y⟫_𝕜 = (⟪T (x + y), x + y⟫_𝕜 - ⟪T (x - y), x - y⟫_𝕜 - IsROrC.I * ⟪T (x + IsROrC.I • y), x + IsROrC.I • y⟫_𝕜 + IsROrC.I * ⟪T (x - IsROrC.I • y), x - IsROrC.I • y⟫_𝕜) / 4

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

theorem LinearMap.IsSymmetric.inner_map_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) : (∀ (x : E), ⟪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.