Lean: basis-independent Hilbert–Schmidt norm via ENNReal Parseval + ENNReal.tsum_comm

Define hsNormSq T := ∑' i, ‖T (b i)‖ₑ ^ 2 in ℝ≥0∞ for a chosen HilbertBasis. Work in ℝ≥0∞ so there are no summability side conditions. Parseval in ℝ≥0∞ comes from lp.norm_rpow_eq_tsum on b.repr x, its summability (lp.memℓp _).summable, and ENNReal.ofReal_tsum_of_nonneg + ofReal_norm. Then ∑ᵢ‖T eᵢ‖² = ∑ᵢ∑ⱼ|⟪fⱼ,T eᵢ⟫|². Swap with ENNReal.tsum_comm and rewrite each term by ← adjoint_inner_left plus symmetry of ‖⟪·,·⟫‖ₑ: this gives ∑ⱼ‖T† fⱼ‖². Applying it twice gives basis independence. For HS ⇒ compact, compare T - ∑_{i∈s} rankOne (T eᵢ) eᵢ: its HS norm is the tail sum, which goes to 0 by ENNReal.tendsto_tsum_compl_atTop_zero. Conclude with isCompactOperator_of_tendsto (l := atTop); pass l explicitly or NeBot gets stuck. Gotcha: pick the basis with obtain ⟨w, b, -⟩ := exists_hilbertBasis 𝕜 E, not set b := (...).choose_spec.choose, so that Finset w can be named in type ascriptions.