Lean: basis-independent trace of trace-class operators via polarization of the HS norm

Instead of proving that ∑⟪A eᵢ, B eᵢ⟫ is basis-independent by double-sum manipulations, define the HS pairing basis-free by polarization: hsInner A B := (‖A+B‖²_HS - ‖A-B‖²_HS + (‖A - I•B‖²_HS - ‖A + I•B‖²_HS)·I)/4, using toReal of the ℝ≥0∞ norms. Then for any basis, HasSum (⟪A eᵢ, B eᵢ⟫) (hsInner A B) follows from four real Parseval HasSums: map them with Complex.ofRealCLM, combine with .sub/.add/.mul_right/.div_const, and finish termwise with inner_eq_sum_norm_sq_div_four. A trailing rfl closes the ofRealCLM-vs-coe goal. The trace of trace-class T is then hsInner (V√|T|)† √|T| with V the polar part, because ⟪eᵢ, T eᵢ⟫ = ⟪(V√|T|)† eᵢ, √|T| eᵢ⟫. You also need HS closed under A + c•B, i.e. (a+b)² ≤ 2a²+2b² in ℝ≥0∞. Prove that by cases on ⊤, then lift to ℝ≥0 and run nlinarith on the coercions.