Trace function convex univ

theorem trace_function_convex_univ (g : ℝ → ℝ) (hg : ConvexOn ℝ Set.univ g) :    ConvexOn ℝ Set.univ (fun A : HermitianMat d ℂ => (A.cfc g).trace) := by  refine ⟨convex_univ, ?_⟩  intro A _ B _ a b ha hb hab;  -- Let $C = aA + bB$.  set C : HermitianMat d ℂ := a • A + b • B;  -- By the properties of the trace and the convexity of $g$, we have:  have h_trace : (C.cfc g).trace = ∑ i, g (C.H.eigenvalues i) := by    exact trace_cfc_eq C g;  -- By the properties of the trace and the convexity of $g$, we have $\sum_{i} g(C_{ii}) \leq a \sum_{i} g(A_{ii}) + b \sum_{i} g(B_{ii})$.  have h_sum : ∑ i, g (C.H.eigenvalues i) ≤ a * ∑ i, g ((A.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) + b * ∑ i, g ((B.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) := by    have h_sum : ∀ i, g (C.H.eigenvalues i) ≤ a * g ((A.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) + b * g ((B.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) := by      intro i      have h_eigenvalue : C.H.eigenvalues i = a * ((A.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) + b * ((B.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) := by        have h_eigenvalue : (C.conj (star C.H.eigenvectorUnitary.val)).mat i i = a * (A.conj (star C.H.eigenvectorUnitary.val)).mat i i + b * (B.conj (star C.H.eigenvectorUnitary.val)).mat i i := by          simp +zetaDelta at *;          simp [conj]          exact Complex.ext rfl rfl;        have h_eigenvalue : (C.conj (star C.H.eigenvectorUnitary.val)) = (diagonal ℂ C.H.eigenvalues).conj 1 := by          have h_eigenvalue : C = (diagonal ℂ C.H.eigenvalues).conj C.H.eigenvectorUnitary := by            exact eq_conj_diagonal C;          convert congr_arg ( fun x => ( conj ( star C.H.eigenvectorUnitary.val ) ) x ) h_eigenvalue using 1;          simp [ HermitianMat.conj_conj ];        simp_all [ HermitianMat.conj ];        convert congr_arg Complex.re ‹ ( diagonal ℂ _ ) i i = _ › using 1;        · exact Eq.symm ( by erw [ show ( diagonal ℂ _ : HermitianMat d ℂ ) i i = ( C.H.eigenvalues i : ℂ ) by exact if_pos rfl ] ; norm_cast );        · norm_num [ Complex.ext_iff ];      rw [h_eigenvalue]      exact hg.2 trivial trivial ha hb hab;    simpa only [ Finset.mul_sum _ _ _, Finset.sum_add_distrib ] using Finset.sum_le_sum fun i _ => h_sum i;  -- By the properties of the trace and the convexity of $g$, we have $\sum_{i} g(A_{ii}) \leq \text{tr}(g(A))$ and $\sum_{i} g(B_{ii}) \leq \text{tr}(g(B))$.  have h_trace_A : ∑ i, g ((A.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) ≤ (A.cfc g).trace := by    convert HermitianMat.peierls_inequality _ _ hg using 1;    convert HermitianMat.trace_cfc_conj_unitary _ _ _ using 1;    rotate_right;    exact C.H.eigenvectorUnitary;    simp [ conj_conj ]  have h_trace_B : ∑ i, g ((B.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) ≤ (B.cfc g).trace := by    convert HermitianMat.peierls_inequality _ _ hg using 1;    convert HermitianMat.trace_cfc_conj_unitary _ _ _;    rotate_right;    exact C.H.eigenvectorUnitary;    simp [ conj_conj ];  simpa only [ h_trace ] using h_sum.trans ( add_le_add ( mul_le_mul_of_nonneg_left h_trace_A ha ) ( mul_le_mul_of_nonneg_left h_trace_B hb ) )