Inner rho H hat

theorem inner_rho_H_hat (hα : 1 < α) (ρ σ : MState d) :    let γ := (1 - α) / (2 * α)    ⟪ρ.M, H_hat α ρ σ⟫_ℝ = ((ρ.M.conj (σ.M ^ γ).mat) ^ α).trace := by  unfold H_hat; simp [ HermitianMat.inner_def ] ;  have h_cyclic : (ρ.m * (σ.M ^ ((1 - α) / (2 * α))).mat * ((ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat) ^ (α - 1)).mat * (σ.M ^ ((1 - α) / (2 * α))).mat).trace = ((ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat) ^ α).trace := by    have h_cyclic : (ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat).mat * ((ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat) ^ (α - 1)).mat = ((ρ.M.conj (σ.M ^ ((1 - α) / (2 * α))).mat) ^ α).mat := by      have := @HermitianMat.mat_rpow_add;      specialize this ( show 0 ≤ HermitianMat.conj ( σ.M ^ ( ( 1 - α ) / ( 2 * α ) ) ).mat ρ.M from ?_ ) ( show ( 1 : ℝ ) + ( α - 1 ) ≠ 0 from by linarith );      · positivity      · aesop;    convert congr_arg Matrix.trace h_cyclic using 1;    · rw [ ← Matrix.trace_mul_comm ] ; simp [ Matrix.mul_assoc ] ;    · simp [ HermitianMat.trace ];      norm_num [ Matrix.trace ];      refine Finset.sum_congr rfl fun i _ => ?_      convert Complex.ofReal_re (( ( HermitianMat.conj ( σ.M ^ ( ( 1 - α ) / ( 2 * α ) ) ).mat ) ρ.M ^ α ) i i |> Complex.re)      simp [ Complex.ext_iff ];  simp_all [ ← Matrix.mul_assoc ]