Sandwiched Aux Fun concave in H

lemma sandwichedAuxFun_concave_in_H (hα : 1 < α) (ρ σ : MState d) :    ConcaveOn ℝ {H | 0 ≤ H} (fun H => f_alpha α H ρ σ) := by  constructor  · rw [convex_iff_forall_pos]    exact fun x hx y hy a b ha hb hab => by simpa [ hab ] using add_nonneg ( smul_nonneg ha.le hx ) ( smul_nonneg hb.le hy ) ;  · intro x hx y hy a b ha hb hab    simp [f_alpha];    -- Apply the convexity of the trace function composed with rpow.    have h_trace_convex : ConvexOn ℝ {A : HermitianMat d ℂ | 0 ≤ A} (fun A => (A ^ (α / (α - 1))).trace) := by      have h_trace_convex : ConvexOn ℝ (Set.Ici 0) (fun x : ℝ => x ^ (α / (α - 1))) := by        exact ( convexOn_rpow ( by rw [ le_div_iff₀ ] <;> linarith ) );      convert HermitianMat.trace_function_convex_ici h_trace_convex using 1;    have := h_trace_convex.2 ( show 0 ≤ ( HermitianMat.conj ( σ.M ^ ( - ( ( 1 - α ) / ( 2 * α ) ) ) ) x ) from ?_ ) ( show 0 ≤ ( HermitianMat.conj ( σ.M ^ ( - ( ( 1 - α ) / ( 2 * α ) ) ) ) y ) from ?_ ) ha hb hab;    · simp_all +decide [ inner_add_right, inner_smul_right, HermitianMat.conj ];      nlinarith! [ show 0 ≤ α - 1 by linarith ];    · apply_rules [ HermitianMat.conj_nonneg ];    · apply_rules [ HermitianMat.conj_nonneg ]