F alpha convex in sigma

theorem f_alpha_convex_in_sigma (hα : 1 < α) (H : HermitianMat d ℂ) (hH : 0 ≤ H)    (ρ : MState d) {ι : Type*} [Fintype ι]    (w : ι → ℝ) (hw_nonneg : ∀ i, 0 ≤ w i) (hw_sum : ∑ i, w i = 1)    (σs : ι → MState d) (σ_mix : MState d)    (hσ_mix : σ_mix.M = ∑ i, w i • (σs i).M) :    f_alpha α H ρ σ_mix ≤ ∑ i, w i * f_alpha α H ρ (σs i) := by  have hα_pos : 0 < α - 1 := by linarith  -- Define the σ-dependent trace function on HermitianMat  let s := (α - 1) / (2 * α)  let p := α / (α - 1)  let F : HermitianMat d ℂ → ℝ := fun σ => ((H.conj (σ ^ s).mat) ^ p).trace  -- f_alpha relates to F via: f_alpha α H ρ σ = α * ⟪ρ.M, H⟫ - (α-1) * F(σ.M)  -- because -γ = -((1-α)/(2α)) = (α-1)/(2α) = s  have hf_eq : ∀ σ : MState d, f_alpha α H ρ σ = α * ⟪ρ.M, H⟫_ℝ - (α - 1) * F σ.M := by    intro σ    show _ = α * ⟪ρ.M, H⟫_ℝ - (α - 1) *      ((H.conj (σ.M ^ ((α - 1) / (2 * α))).mat) ^ (α / (α - 1))).trace    unfold f_alpha; ring_nf  simp_rw [hf_eq]  -- Reduce to concavity: ∑ w_i * F(σ_i.M) ≤ F(σ_mix.M)  suffices h : ∑ i, w i * F (σs i).M ≤ F σ_mix.M by    have h1 : ∑ i, w i * ((α - 1) * F (σs i).M) = (α - 1) * ∑ i, w i * F (σs i).M := by      rw [Finset.mul_sum]; congr 1; ext i; ring    simp only [mul_sub, Finset.sum_sub_distrib, ← Finset.sum_mul, hw_sum, one_mul, h1]    linarith [mul_le_mul_of_nonneg_left h (le_of_lt hα_pos)]  -- Apply ConcaveOn.le_map_sum from trace_conj_rpow_concave  have hF_concave : ConcaveOn ℝ {σ : HermitianMat d ℂ | 0 ≤ σ} F :=    trace_conj_rpow_concave hα H hH  have h_jensen := hF_concave.le_map_sum    (t := Finset.univ) (w := w) (p := fun i => (σs i).M)    (fun i _ => hw_nonneg i)    (by simp [hw_sum])    (fun i _ => (σs i).nonneg)  rw [← hσ_mix] at h_jensen  convert h_jensen using 1