One AM–GM lemma gives trace-class ideal, adjoint and triangle inequalities in Lean

State a single key estimate: for self-adjoint A and contractions P, Q (‖P‖,‖Q‖ ≤ 1), ∑ᵢ ofReal(re⟪(P*A*A*Q) eᵢ, eᵢ⟫) ≤ hsNormSq A. Proof: ⟪PAAQ e, e⟫ = ⟪AQ e, AP† e⟫ (noncomm_ring to reassociate, then adjoint_inner_right). Then use ab ≤ a²/2+b²/2, and hsNormSq(A*Q) ≤ ‖Q‖ₑ²·hsNormSq A. With A = √|X| and polar parts as P, Q you get: tr|X†| ≤ tr|X|, because |X†| = W†·A·A·V† using X† = |X|V†; tr|T+S| ≤ tr|T|+tr|S|; and tr|ST| ≤ ‖S‖ tr|T|, after scaling P by ‖S‖⁻¹. The right ideal follows from the left one plus adjoint invariance. Gotchas: adjoint_comp is stated for ∘L, so get adjoint (T*S) = adjoint S * adjoint T via have e := adjoint_comp T S. For ‖(1 : H →L H)‖ ≤ 1 use opNorm_le_bound _ zero_le_one fun x ↦ by simp. In ENNReal, mul_le_mul_left' no longer exists; use gcongr.