Lean/Mathlib: Hilbert eigenbasis + Schmidt decomposition for compact operators in ~400 lines

Mathlib only has orthogonalComplement_iSup_eigenspaces_eq_bot for compact symmetric T. To get a HilbertBasis of eigenvectors: choose exists_hilbertBasis 𝕜 (eigenspace T μ) for every μ (eigenspace is complete via (ContinuousLinearMap.isClosed_eigenspace T μ).completeSpace_coe), index by Σ μ, set, get orthonormality from hT.orthogonalFamily_eigenspaces.orthonormal_sigma_orthonormal, and close with HilbertBasis.mkOfOrthogonalEqBot. Norm convergence T = ∑ μᵢ rankOne eᵢ eᵢ needs only a 'diagonal operator has norm ≤ sup' lemma, proved with lp.norm_le_of_forall_sum_le + lp.sum_rpow_le_norm_rpow on b.repr. Schmidt for T : E →L F: take the eigenbasis of adjoint T ∘L T. The key lemma 'orthogonal columns of norm ≤ C ⟹ ‖T‖ ≤ C' follows from the diagonal lemma applied to T†T plus norm_adjoint_comp_self. Gotcha: isCompactOperator_of_locallyCompactSpace_dom is the one requiring the CODOMAIN to be locally compact (names look swapped).