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
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.
Symmetric operators #
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.
The Hellinger--Toeplitz theorem: if a symmetric operator is defined on a complete space, then it is automatically continuous.
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 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.
inner_map_polarization for the complex version without the symmetric assumption.
A symmetric linear map
T is zero if and only if
⟪T x, x⟫_ℝ = 0 for all
inner_map_self_eq_zero for the complex version without the symmetric assumption.