simple linear algebra

Stream: new members

[Monica Omar]

I'm currently stuck on this one problem. Any help would be appreciated!

import analysis.inner_product_space.spectrum

open_locale big_operators
lemma hi {n : ℕ} {V : Type*} [inner_product_space ℂ V]  [finite_dimensional ℂ V] (T : V →ₗ[ℂ] V) (x : V)
  (hT : T.is_symmetric) (hn : finite_dimensional.finrank ℂ V = n) (h : ∀ i, 0 ≤ hT.eigenvalues hn i) :
  0 ≤ ∑ i : fin n, (real.sqrt (hT.eigenvalues hn i) • (⟪x, hT.eigenvector_basis hn i⟫_ℂ * ⟪hT.eigenvector_basis hn i, x⟫_ℂ)).re := sorry

[Ruben Van de Velde]

Start with docs#finset.sum_nonneg?

[Eric Wieser]

 simp_rw [←inner_conj_sym x, ←complex.norm_sq_eq_conj_mul_self, complex.smul_re,
    complex.of_real_re, smul_eq_mul],

makes some good progress, then it's a trivial inequality