Hermitian Mat inner le trace rpow mul

lemma HermitianMat.inner_le_trace_rpow_mul    {A B : HermitianMat d ℂ} (hA : 0 ≤ A) (hB : 0 ≤ B)    (p q : ℝ) (hp : 1 < p) (hpq : 1/p + 1/q = 1) :    ⟪A, B⟫_ℝ ≤ (A ^ p).trace ^ (1/p) * (B ^ q).trace ^ (1/q) := by  by_cases hq : q > 1;  · -- Apply the doubly_stochastic_holder lemma with the weights $w_{ij} = \|C_{ij}\|^2$.    rw [trace_rpow_eq_sum, trace_rpow_eq_sum, inner_eq_doubly_stochastic_sum]    refine doubly_stochastic_holder      A.H.eigenvalues B.H.eigenvalues      (fun i j ↦ ‖(A.H.eigenvectorUnitary.val.conjTranspose * B.H.eigenvectorUnitary.val) i j‖ ^ 2)      (fun i ↦ by simpa using hA.eigenvalues_nonneg i)      (fun i ↦ by simpa using hB.eigenvalues_nonneg i)      (by bound) ?_ ?_ p q hp hpq    · apply Matrix.unitary_row_sum_norm_sq (A.H.eigenvectorUnitary.val.conjTranspose * B.H.eigenvectorUnitary.val)      simp [mul_assoc]      simp [← mul_assoc, Matrix.IsHermitian.eigenvectorUnitary]    · apply Matrix.unitary_col_sum_norm_sq (A.H.eigenvectorUnitary.val.conjTranspose * B.H.eigenvectorUnitary.val)      simp [mul_assoc]      simp [← mul_assoc, Matrix.IsHermitian.eigenvectorUnitary]  · rcases eq_or_ne q 0 with _ | _    · grind only [cases Or]    · field_simp at hpq      nlinarith