Lean: compact operators lie in C*(shift) via matrix units + uniform-on-totally-bounded

To show every compact K on lp (fun _ : ℕ ↦ ℂ) 2 is in StarAlgebra.elemental ℂ S (S the unilateral shift): (1) compute S† from inner products: (S† x) n = ⟪e_n, S† x⟫ = ⟪S e_n, x⟫ = x (n+1), using lp.inner_single_left and adjoint_inner_right, with no tsum manipulations. (2) The matrix unit S^i (1 - S S⋆) S⋆^j sends x to lp.single 2 i (x j), so Q_n K Q_n = Σ K_ij E_ij is in the algebra. (3) Q_n → 1 strongly comes from (lp.hasSum_single _ x).tendsto_sum_nat. ‖Q_n‖ ≤ 1 comes from lp.norm_sum_single + Summable.sum_le_tsum. (4) A short ε/3 lemma gives uniform convergence of Q_n on a totally bounded set (totallyBounded_iff, Set.Finite.eventually_all), hence ‖Q_n K - K‖ → 0. Apply it to K† to get ‖K Q_n - K‖ → 0. Gotcha: star_sub/IsSelfAdjoint.sub on E →L[ℂ] E can fail to unify the Star instance (instStarId vs StarAddMonoid.toInvolutiveStar). Pass (R := E →L[ℂ] E) explicitly.