Peierls inequality

theorem peierls_inequality (A : HermitianMat d ℂ) (g : ℝ → ℝ) (hg : ConvexOn ℝ Set.univ g) :    ∑ i, g ((A.mat i i).re) ≤ (A.cfc g).trace := by  -- By the properties of the trace and the convexity of $g$, we have:  have h_trace_le : ∑ i, g ((A.mat i i).re) ≤ ∑ j, g (A.H.eigenvalues j) * ∑ i, ‖(A.H.eigenvectorUnitary.val i j)‖^2 := by    -- By the spectral theorem, we can write $A$ as $A = \sum_{i} \lambda_i u_i u_i^*$, where $\lambda_i$ are the eigenvalues and $u_i$ are the corresponding eigenvectors.    have h_spectral : ∀ i, (A.mat i i).re = ∑ j, A.H.eigenvalues j * ‖(A.H.eigenvectorUnitary.val i j)‖^2 := by      intro i      have h_sum : (A.mat i i).re = ∑ j, (A.H.eigenvectorBasis j i) * star (A.H.eigenvectorBasis j i) * A.H.eigenvalues j := by        have := A.H.spectral_theorem;        replace this := congr_fun ( congr_fun this i ) i ; simp_all [ Matrix.mul_apply, Matrix.diagonal ] ;        simp [ Complex.ext_iff, mul_comm, mul_left_comm ];        exact Finset.sum_congr rfl fun _ _ => by ring;      simp_all [ Complex.ext_iff, mul_comm ];      simp [ Complex.normSq, Complex.sq_norm ];    have h_jensen : ∀ i, g ((A.mat i i).re) ≤ ∑ j, ‖(A.H.eigenvectorUnitary.val i j)‖^2 * g (A.H.eigenvalues j) := by      intro i      have h_convex_comb : ∑ j, ‖(A.H.eigenvectorUnitary.val i j)‖^2 = 1 := by        have := A.H.eigenvectorUnitary.2;        have := this.2;        replace this := congr_fun ( congr_fun this i ) i; simp_all [ Matrix.mul_apply, Complex.mul_conj, Complex.normSq_eq_norm_sq ] ;        exact_mod_cast this;      convert hg.map_sum_le _ _ _ <;> simp_all [ mul_comm ];    convert Finset.sum_le_sum fun i _ => h_jensen i using 1;    rw [ Finset.sum_comm, Finset.sum_congr rfl ] ; intros ; rw [ Finset.mul_sum _ _ _ ] ; ac_rfl;  have h_unitary : ∀ (j : d), ∑ i, ‖(A.H.eigenvectorUnitary.val i j)‖^2 = 1 := by    exact fun j => Matrix.unitaryGroup_row_norm (H A).eigenvectorUnitary j;  simp_all [ HermitianMat.trace_cfc_eq ]