Documentation

Mathlib.Analysis.InnerProductSpace.Symmetric

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} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) :

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

Instances For

theorem LinearMap.isSymmetric_iff_sesqForm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) :

T.IsSymmetric ↔ (innerₛₗ 𝕜).flip.IsSelfAdjoint ⇑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} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x y : E) :

(starRingEnd 𝕜) (inner 𝕜 (T x) y) = inner 𝕜 (T y) x

@[simp]

theorem LinearMap.IsSymmetric.apply_clm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (hT : (↑T).IsSymmetric) (x y : E) :

inner 𝕜 (T x) y = inner 𝕜 x (T y)

@[simp]

theorem LinearMap.IsSymmetric.zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

@[simp]

theorem LinearMap.IsSymmetric.id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

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

(T + S).IsSymmetric

theorem LinearMap.isSymmetric_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_3} {T : ι → E →ₗ[𝕜] E} (s : Finset ι) (hT : ∀ i ∈ s, (T i).IsSymmetric) :

(∑ i ∈ s, T i).IsSymmetric

theorem LinearMap.IsSymmetric.sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) :

(T - S).IsSymmetric

theorem LinearMap.IsSymmetric.smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {c : 𝕜} (hc : (starRingEnd 𝕜) c = c) {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :

(c • T).IsSymmetric

theorem LinearMap.IsSymmetric.natCast {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (n : ℕ) :

(↑n).IsSymmetric

theorem LinearMap.IsSymmetric.intCast {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (n : ℤ) :

(↑n).IsSymmetric

theorem LinearMap.IsSymmetric.mul_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S T : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (hT : T.IsSymmetric) (hST : Commute S T) :

(S * T).IsSymmetric

theorem LinearMap.IsSymmetric.pow {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (n : ℕ) :

(T ^ n).IsSymmetric

@[simp]

theorem LinearMap.IsSymmetric.coe_reApplyInnerSelf_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (hT : (↑T).IsSymmetric) (x : E) :

↑(T.reApplyInnerSelf x) = inner 𝕜 (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} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {V : Submodule 𝕜 E} (hV : ∀ v ∈ V, T v ∈ V) :

(T.restrict hV).IsSymmetric

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} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :

(↑ℝ T).IsSymmetric

@[simp]

theorem LinearMap.IsSymmetric.im_inner_apply_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) :

RCLike.im (inner 𝕜 (T x) x) = 0

@[simp]

theorem LinearMap.IsSymmetric.im_inner_self_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) :

RCLike.im (inner 𝕜 x (T x)) = 0

@[simp]

theorem LinearMap.IsSymmetric.coe_re_inner_apply_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) :

↑(RCLike.re (inner 𝕜 (T x) x)) = inner 𝕜 (T x) x

@[simp]

theorem LinearMap.IsSymmetric.coe_re_inner_self_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x : E) :

↑(RCLike.re (inner 𝕜 x (T x))) = inner 𝕜 x (T x)

structure LinearMap.IsSymmetricProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) :

A symmetric projection is a symmetric idempotent.

isIdempotentElem : IsIdempotentElem T
isSymmetric : T.IsSymmetric

Instances For

theorem LinearMap.isSymmetricProjection_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) :

T.IsSymmetricProjection ↔ IsIdempotentElem T ∧ T.IsSymmetric

theorem LinearMap.isSymmetric_iff_inner_map_self_real {V : Type u_3} [SeminormedAddCommGroup V] [InnerProductSpace ℂ V] (T : V →ₗ[ℂ ] V) :

T.IsSymmetric ↔ ∀ (v : V), (starRingEnd ℂ) (inner ℂ (T v) v) = 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.

theorem LinearMap.IsSymmetric.inner_map_polarization {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (x y : E) :

inner 𝕜 (T x) y = (inner 𝕜 (T (x + y)) (x + y) - inner 𝕜 (T (x - y)) (x - y) - RCLike.I * inner 𝕜 (T (x + RCLike.I • y)) (x + RCLike.I • y) + RCLike.I * inner 𝕜 (T (x - RCLike.I • y)) (x - RCLike.I • y)) / 4

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

theorem LinearMap.isSymmetric_linearIsometryEquiv_conj_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →ₗ[𝕜] E) (f : E ≃ₗᵢ[𝕜] F) :

(↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv).IsSymmetric ↔ T.IsSymmetric

@[simp]

theorem InnerProductSpace.isSymmetric_rankOne_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

(↑(((rankOne 𝕜) x) x)).IsSymmetric

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

(↑(((rankOne 𝕜) x) x)).IsSymmetricProjection

theorem LinearMap.IsSymmetric.toLinearMap_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E ≃ₗ[𝕜] E} (hT : (↑T).IsSymmetric) :

(↑T.symm).IsSymmetric

@[simp]

theorem LinearEquiv.isSymmetric_symm_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E ≃ₗ[𝕜] E} :

(↑T.symm).IsSymmetric ↔ (↑T).IsSymmetric

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

Continuous ⇑T

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

theorem LinearMap.IsSymmetric.inner_map_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :

(∀ (x : E), 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.

theorem LinearMap.ker_le_ker_of_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S T : E →ₗ[𝕜] E} (hS : S.IsSymmetric) (hT : T.IsSymmetric) (h : S.range ≤ T.range) :

T.ker ≤ S.ker

theorem Submodule.IsCompl.projection_isSymmetric_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} (hUV : IsCompl U V) :

(projection hUV).IsSymmetric ↔ U ⟂ V

A linear projection onto U along its complement V is symmetric if and only if U and V are pairwise orthogonal.

theorem Submodule.IsCompl.projection_isSymmetricProjection_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} (hUV : IsCompl U V) :

(projection hUV).IsSymmetricProjection ↔ U ⟂ V

theorem Submodule.IsCompl.projection_isSymmetricProjection_of_isOrtho {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} (hUV : IsCompl U V) :

U ⟂ V → (projection hUV).IsSymmetricProjection

Alias of the reverse direction of Submodule.IsCompl.projection_isSymmetricProjection_iff.

theorem LinearMap.IsIdempotentElem.isSymmetric_iff_isOrtho_range_ker {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : IsIdempotentElem T) :

T.IsSymmetric ↔ T.range ⟂ T.ker

An idempotent operator is symmetric if and only if its range is pairwise orthogonal to its kernel.

theorem LinearMap.IsSymmetric.orthogonal_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :

T.rangeᗮ = T.ker

theorem LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (h : IsIdempotentElem T) :

T.IsSymmetric ↔ T.rangeᗮ = T.ker

theorem LinearMap.IsSymmetricProjection.ext_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S T : E →ₗ[𝕜] E} (hS : S.IsSymmetricProjection) (hT : T.IsSymmetricProjection) :

S = T ↔ S.range = T.range

Symmetric projections are equal iff their range are.

theorem LinearMap.IsSymmetricProjection.ext {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S T : E →ₗ[𝕜] E} (hS : S.IsSymmetricProjection) (hT : T.IsSymmetricProjection) :

S.range = T.range → S = T

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

Symmetric projections are equal iff their range are.

theorem LinearMap.IsSymmetricProjection.sub_of_range_le_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) (hqp : p.range ≤ q.range) :

(q - p).IsSymmetricProjection

theorem LinearMap.IsSymmetric.isSymmetric_smul_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {f : E →ₗ[𝕜] E} (hf : f.IsSymmetric) (hf' : f ≠ 0) {α : 𝕜} :

(α • f).IsSymmetric ↔ IsSelfAdjoint α

@[deprecated LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range (since := "2025-12-28")]

theorem ContinuousLinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (h : IsIdempotentElem T) :

T.IsSymmetric ↔ T.rangeᗮ = T.ker

Alias of LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range.