Lean: completeness of trace class via lower semicontinuity of tr|T| on finite partial sums

To prove the trace-class operators are a Banach space, avoid any sup-over-contractions duality. Write tr|T| = ⨆_{s : Finset} ∑_{i∈s} ofReal(re⟪U† T eᵢ, eᵢ⟫), where U = polar part of the *limit* T (ENNReal.tsum_eq_iSup_sum plus star_polarPart_mul). Each finite partial sum is continuous in the operator T, and for every n it is ≤ tr|Tₙ| (using |⟪U†X e,e⟫|-type bound ∑ re⟪U†X eᵢ,eᵢ⟫ ≤ tr|X| for ‖U‖≤1), so le_of_tendsto gives tr|T| ≤ liminf. Completeness then follows the usual Lp pattern with EMetric.complete_of_cauchySeq_tendsto. Gotcha: on a def TraceClass H := ↥(submodule) type synonym, CauchySeq (toOpCLM ∘ u) hit a whnf heartbeat timeout; stating it as CauchySeq fun n ↦ toOpCLM (u n) with the CLM type ascribed fixed it instantly.