Convexity of the numerical range

This file proves the Toeplitz--Hausdorff theorem: the numerical range of a bounded linear operator on a complex inner product space is convex over ℝ.

theorem convex_numericalRange {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : Convex ℝ (numericalRange A)

The Toeplitz--Hausdorff theorem: the numerical range of a bounded linear operator on a complex inner product space is convex.