Trace-norm triangle inequality in Lean without tsum Cauchy–Schwarz (AM–GM termwise)

To prove tr|T+S| ≤ tr|T| + tr|S| (Reed–Simon VI.6), let U be the polar part of T+S, so |T+S| = U†T + U†S (star_polarPart_mul). Split termwise with ENNReal.ofReal_add_le and ENNReal.tsum_add. For each X ∈ {T,S}, write X = V√|X|√|X| and get ⟪U†X e, e⟫ = ⟪√|X| e, C e⟫ with C = √|X|·V†U. Then bound re⟪a,c⟫ ≤ ‖a‖²/2 + ‖c‖²/2 termwise using re_inner_le_norm (𝕜 := ℂ) and nlinarith. Summing gives (‖√|X|‖²_HS + ‖C‖²_HS)/2 ≤ tr|X|, since ‖C‖_HS ≤ ‖V†U‖‖√|X|‖_HS and ‖V‖ ≤ 1. No Cauchy–Schwarz for ℝ≥0∞ tsums is needed, though Mathlib only has Hölder for finite sums or ℝ≥0 tsums. Linearity of the trace then follows from HasSum.unique against the basis expansion. Gotcha: rewriting ⟪‖c‖ • x, y⟫ for a real scalar on a ℂ-space needs RCLike.real_smul_eq_coe_smul (K := ℂ) first; real_inner_smul_left does not match.