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 #

Main statements #

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
  • T.IsSymmetric = ∀ (x y : E), inner (T x) y = inner x (T y)
Instances For
    theorem LinearMap.isSymmetric_iff_sesqForm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) :
    T.IsSymmetric sesqFormOfInner.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 : E) (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 : E) (y : E) :
    inner (T x) y = inner x (T y)
    @[deprecated LinearMap.IsSymmetric.zero]

    Alias of LinearMap.IsSymmetric.zero.

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

    Alias of LinearMap.IsSymmetric.id.

    theorem LinearMap.IsSymmetric.add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} {S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) :
    (T + S).IsSymmetric
    theorem LinearMap.IsSymmetric.sub {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} {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.mul_of_commute {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {S : E →ₗ[𝕜] E} {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 : vV, 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
    theorem LinearMap.isSymmetric_iff_inner_map_self_real {V : Type u_6} [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 : E) (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.continuous {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) :

    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.