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 allx
,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 #
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
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.
For a symmetric operator T
, the function fun x ↦ ⟪T x, x⟫
is real-valued.
If a symmetric operator preserves a submodule, its restriction to that submodule is symmetric.
A symmetric projection is a symmetric idempotent.
- isIdempotentElem : IsIdempotentElem T
- isSymmetric : T.IsSymmetric
Instances For
A linear operator on a complex inner product space is symmetric precisely when
⟪T v, v⟫_ℂ
is real for all v.
Polarization identity for symmetric linear maps.
See inner_map_polarization
for the complex version without the symmetric assumption.
The Hellinger--Toeplitz theorem: if a symmetric operator is defined on a complete space, then it is automatically continuous.
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.
A linear projection onto U
along its complement V
is symmetric if
and only if U
and V
are pairwise orthogonal.
Alias of the reverse direction of Submodule.IsCompl.projection_isSymmetricProjection_iff
.
An idempotent operator is symmetric if and only if its range is pairwise orthogonal to its kernel.
Symmetric projections are equal iff their range are.
Alias of the reverse direction of LinearMap.IsSymmetricProjection.ext_iff
.
Symmetric projections are equal iff their range are.
An idempotent operator T
is symmetric iff (range T)ᗮ = ker T
.