feat(analysis/inner_product_space/adjoint): gram lemmas (#12139)

The gram operator is a self-adjoint, positive operator.



Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>

src/analysis/inner_product_space/adjoint.lean

@@ -298,6 +298,20 @@ lemma is_adjoint_pair (A : E' →ₗ[ℝ] F') :
 
 end real
 
+/-- The Gram operator T†T is self-adjoint. -/
+lemma is_self_adjoint_adjoint_mul_self (T : E →ₗ[𝕜] E) : is_self_adjoint (T.adjoint * T) :=
+λ x y, by simp only [linear_map.mul_apply, linear_map.adjoint_inner_left,
+  linear_map.adjoint_inner_right]
+
+/-- The Gram operator T†T is a positive operator. -/
+lemma re_inner_adjoint_mul_self_nonneg (T : E →ₗ[𝕜] E) (x : E) :
+  0 ≤ is_R_or_C.re ⟪ x, (T.adjoint * T) x ⟫ := by {simp only [linear_map.mul_apply,
+  linear_map.adjoint_inner_right, inner_self_eq_norm_sq_to_K], norm_cast, exact sq_nonneg _}
+
+@[simp] lemma im_inner_adjoint_mul_self_eq_zero (T : E →ₗ[𝕜] E) (x : E) :
+  is_R_or_C.im ⟪ x, linear_map.adjoint T (T x) ⟫ = 0 := by {simp only [linear_map.mul_apply,
+    linear_map.adjoint_inner_right, inner_self_eq_norm_sq_to_K], norm_cast}
+
 end linear_map
 
 namespace matrix