feat(analysis/inner_product_space): the Hellinger-Toeplitz theorem (#…

…15055)

Prove the Hellinger-Toeplitz theorem as a corollary of the closed graph theorem.

src/analysis/inner_product_space/basic.lean

@@ -7,6 +7,7 @@ import algebra.direct_sum.module
 import analysis.complex.basic
 import analysis.convex.uniform
 import analysis.normed_space.bounded_linear_maps
+import analysis.normed_space.banach
 import linear_algebra.bilinear_form
 import linear_algebra.sesquilinear_form
 
@@ -2300,6 +2301,33 @@ by rw [hT x y, inner_conj_sym]
   ⟪T x, y⟫ = ⟪x, T y⟫ :=
 hT x y
 
+/-- The **Hellinger--Toeplitz theorem**: if a symmetric operator is defined everywhere, then
+  it is automatically continuous. -/
+lemma is_self_adjoint.continuous [complete_space E] {T : E →ₗ[𝕜] E} (hT : is_self_adjoint T) :
+  continuous T :=
+begin
+  -- We prove it by using the closed graph theorem
+  refine T.continuous_of_seq_closed_graph (λ 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 hlhs,
+  rw ←@inner_zero_left 𝕜 E _ _ (T (y - T x)),
+  refine filter.tendsto.inner _ tendsto_const_nhds,
+  rw ←sub_self x,
+  exact hu.sub_const _,
+end
+
+/-- The **Hellinger--Toeplitz theorem**: Construct a self-adjoint operator from an everywhere
+  defined symmetric operator.-/
+def is_self_adjoint.clm [complete_space E] {T : E →ₗ[𝕜] E}
+  (hT : is_self_adjoint T) : E →L[𝕜] E :=
+⟨T, hT.continuous⟩
+
+lemma is_self_adjoint.clm_apply [complete_space E] {T : E →ₗ[𝕜] E}
+  (hT : is_self_adjoint T) {x : E} : hT.clm x = T x := rfl
+
 /-- For a self-adjoint operator `T`, the function `λ x, ⟪T x, x⟫` is real-valued. -/
 @[simp] lemma is_self_adjoint.coe_re_apply_inner_self_apply
   {T : E →L[𝕜] E} (hT : is_self_adjoint (T : E →ₗ[𝕜] E)) (x : E) :