Trace function convex ici

theorem trace_function_convex_ici {g : ℝ → ℝ} (hg : ConvexOn ℝ (Set.Ici 0) g) :    ConvexOn ℝ {A : HermitianMat d ℂ | 0 ≤ A} (fun A => (A.cfc g).trace) := by  refine ⟨convex_Ici 0, ?_⟩  intro A hA B hB 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 only [mat_add, mat_smul, map_add, mat_apply]          simp only [conj, AddMonoidHom.coe_mk, ZeroHom.coe_mk, mat_smul, Algebra.mul_smul_comm,            Algebra.smul_mul_assoc]          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]      refine hg.2 ?_ ?_ ha hb hab      · simp        exact (Complex.le_def.mp (((zero_le_iff.mp (conj_nonneg _ hA)).diag_nonneg (i := i)))).1      · simp        exact (Complex.le_def.mp (((zero_le_iff.mp (conj_nonneg _ hB)).diag_nonneg (i := i)))).1    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    have hA' : 0 ≤ A.conj (star C.H.eigenvectorUnitary.val) := A.conj_nonneg _ hA    calc ∑ i, g ((A.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re)        ≤ ((A.conj (star C.H.eigenvectorUnitary.val)).cfc g).trace :=          peierls_inequality_ici _ _ hg hA'      _ = (A.cfc g).trace :=          trace_cfc_conj_unitary A g ⟨star C.H.eigenvectorUnitary.val, by            rw [Matrix.mem_unitaryGroup_iff, star_star]; exact C.H.eigenvectorUnitary.prop.1⟩  have h_trace_B : ∑ i, g ((B.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re) ≤ (B.cfc g).trace := by    have hB' : 0 ≤ B.conj (star C.H.eigenvectorUnitary.val) := B.conj_nonneg _ hB    calc ∑ i, g ((B.conj (star C.H.eigenvectorUnitary.val)).mat i i |> Complex.re)        ≤ ((B.conj (star C.H.eigenvectorUnitary.val)).cfc g).trace :=          peierls_inequality_ici _ _ hg hB'      _ = (B.cfc g).trace :=          trace_cfc_conj_unitary B g ⟨star C.H.eigenvectorUnitary.val, by            rw [Matrix.mem_unitaryGroup_iff, star_star]; exact C.H.eigenvectorUnitary.prop.1⟩  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 ) )