WIP: Fredholm operators for the index pairing (Riesz–Schauder in progress)

[JonBannon]

This is the first step toward proving the chiral Dirac operator $D^+$ is Fredholm, which the general index pairing (thm:index-pairing-well-defined in the blueprint) needs. Mathlib's own Fredholm-operator work (mathlib4#39274) is unmerged, depends on other open PRs, and contains sorrys, so this builds only what's needed directly, with naming chosen to be easy to swap out once the upstream theory lands.

SpectralTriples/CompactOperators.lean adds two Hilbert-space facts about compact operators that Mathlib doesn't currently have:

IsCompactOperator.exists_finiteRank_norm_sub_lt: compact operators are norm-approximable by finite-rank operators (built from a finite $\varepsilon$-net of the relatively compact image of the unit ball, via orthogonal projection onto its span).
IsCompactOperator.adjoint: the adjoint of a compact operator is compact (the adjoints of the finite-rank approximants above are still finite-rank — via ContinuousLinearMap.finiteDimensional_range_adjoint — and converge to $K^\dagger$ in norm, since the adjoint operation is norm-preserving).
Not yet done: the actual Riesz–Schauder theorem — "$1-K$ is Fredholm for $K$ compact" (closed range, finite-dimensional cokernel) — which is what these two lemmas are building toward. That's the next piece, then extending it from $D$ itself to the chiral restriction $D^+$. (I'm actually not sure if it's appropriate to call this Riesz-Schauder, since it is weaker than some of the statements of that theorem one finds online... so I will push on this a bit...)