Sandwiched Trace Functional jointly convex

theorem sandwichedTraceFunctional_jointly_convex (hα : 1 < α) {ι : Type*} [Fintype ι]    (w : ι → ℝ) (hw_nonneg : ∀ i, 0 ≤ w i) (hw_sum : ∑ i, w i = 1)    (ρs σs : ι → MState d) (ρ_mix σ_mix : MState d)    (hρ_mix : ρ_mix.M = ∑ i, w i • (ρs i).M)    (hσ_mix : σ_mix.M = ∑ i, w i • (σs i).M)    (hker : ∀ i, (σs i).M.ker ≤ (ρs i).M.ker) :    Q̃_ α(ρ_mix‖σ_mix) ≤ ∑ i, w i * Q̃_ α(ρs i‖σs i) := by  have hker' : σ_mix.M.ker ≤ ρ_mix.M.ker := by    rw [hρ_mix, hσ_mix]    exact HermitianMat.ker_weighted_sum_le w hw_nonneg _ _ (fun i => (ρs i).nonneg) (fun i => (σs i).nonneg) hker  rw [traceFunctional_eq_iSup_f_alpha hα ρ_mix σ_mix hker']  calc ⨆ H : {H : HermitianMat d ℂ // 0 ≤ H}, f_alpha α H.1 ρ_mix σ_mix      ≤ ∑ i, w i * (⨆ H : {H : HermitianMat d ℂ // 0 ≤ H}, f_alpha α H.1 (ρs i) (σs i)) :=        iSup_f_alpha_jointly_convex hα w hw_nonneg hw_sum ρs σs ρ_mix σ_mix hρ_mix hσ_mix hker    _ = ∑ i, w i * Q̃_ α(ρs i‖σs i) := by        congr 1; ext i        rw [traceFunctional_eq_iSup_f_alpha hα (ρs i) (σs i) (hker i)]