English
Equivalence of symmetry under conjugate-linear transformations with an isometry, reflecting the invariance of symmetry under change of basis.
Русский
Эквивалентность симметричности при сопряжённой линейной эквивалентности, сохраняемой изометрией.
LaTeX
$$$ (f.toLinearMap \circ T \circ f.symm.toLinearMap).IsSymmetric \iff T.IsSymmetric $$$
Lean4
/-- The **Hellinger--Toeplitz theorem**: if a symmetric operator is defined on a complete space,
then it is automatically continuous. -/
theorem continuous [CompleteSpace E] {T : E →ₗ[𝕜] E} (hT : IsSymmetric T) : Continuous T := by
-- We prove it by using the closed graph theorem
refine T.continuous_of_seq_closed_graph fun u x y hu hTu => ?_
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
have hlhs : ∀ k : ℕ, ⟪T (u k) - T x, y - T x⟫ = ⟪u k - x, T (y - T x)⟫ :=
by
intro k
rw [← T.map_sub, hT]
refine tendsto_nhds_unique ((hTu.sub_const _).inner tendsto_const_nhds) ?_
simp_rw [Function.comp_apply, hlhs]
rw [← inner_zero_left (T (y - T x))]
refine Filter.Tendsto.inner ?_ tendsto_const_nhds
rw [← sub_self x]
exact hu.sub_const _
