some obvious lemmas on self-adjoint operators #
This file provides the polarization identity for self adjoint continuous linear maps
over is_R_or_C.
theorem
continuous_linear_map.is_self_adjoint.inner_map_self_eq_zero
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[complete_space E]
{T : E βL[π] E}
(hT : is_self_adjoint T) :
Given a self-adjoint continuous linear operator $T$ on $E$, we get $\langle T x, x \rangle = 0$ for any $x\in E$ if and only if $T=0$.
theorem
continuous_linear_map.is_self_adjoint.inner_map_polarization
{π : Type u_1}
{E : Type u_2}
[is_R_or_C π]
[normed_add_comm_group E]
[inner_product_space π E]
[complete_space E]
{T : E βL[π] E}
(hT : is_self_adjoint T)
(x y : E) :
has_inner.inner (βT x) y = (has_inner.inner (βT (x + y)) (x + y) - has_inner.inner (βT (x - y)) (x - y) - is_R_or_C.I * has_inner.inner (βT (x + is_R_or_C.I β’ y)) (x + is_R_or_C.I β’ y) + is_R_or_C.I * has_inner.inner (βT (x - is_R_or_C.I β’ y)) (x - is_R_or_C.I β’ y)) / 4
The polarization identity for self-adjoint operators.