English
For a linear isometry f, the symmetry of the conjugate-conjugation-transformed operator equals the symmetry of the original operator.
Русский
Для линейного изометрического отображения f симметричность отражения через сопряжение-умножение сохраняется при преобразовании оператора.
LaTeX
$$$ (f.toLinearMap \circ T \circ f.symm.toLinearMap).IsSymmetric \iff T.IsSymmetric $$$
Lean4
/-- A linear operator on a complex inner product space is symmetric precisely when
`⟪T v, v⟫_ℂ` is real for all v. -/
theorem isSymmetric_iff_inner_map_self_real (T : V →ₗ[ℂ] V) : IsSymmetric T ↔ ∀ v : V, conj ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ :=
by
constructor
· intro hT v
apply IsSymmetric.conj_inner_sym hT
· intro h x y
rw [← inner_conj_symm x (T y)]
rw [inner_map_polarization T x y]
simp only [starRingEnd_apply, star_div₀, star_sub, star_add, star_mul]
simp only [← starRingEnd_apply]
rw [h (x + y), h (x - y), h (x + Complex.I • y), h (x - Complex.I • y)]
simp only [Complex.conj_I]
rw [inner_map_polarization']
norm_num
ring
