A = timeBandLimitingOp T W as a bare Module.End, the shape Mathlib's eigenvalue API uses.

The set of eigenvalues of A = timeBandLimitingOp T W lying strictly above c. @audit:ok

For a positive threshold c, the compact operator A has only finitely many eigenvalues above c: an infinite family would give an orthonormal sequence of eigenvectors whose images stay c-separated, contradicting compactness. @audit:ok

The span of all eigenspaces of A whose eigenvalue exceeds c. @audit:ok

The eigenvalue counting function of A: the number of eigenvalues exceeding c, counted with multiplicity.

Only meaningful for 0 < c, where prolateEigenspaceSup_finiteDimensional makes the finrank a genuine dimension. For c ≤ 0 it is a junk value: prolateEigenspaceSup_finiteDimensional no longer applies, and on an infinite-dimensional span finrank reports 0. This is why prolateEigenvalues below takes the infimum over 0 < c rather than 0 ≤ c — the latter would risk letting a junk 0 into the constraint set and collapsing the whole enumeration to ≡ 0. The span's infinite-dimensionality at c ≤ 0 is expected but not established in-tree (at c = 0 it is exactly the open infinite-rank obligation noted on prolateEigenvalues); nothing depends on it, since every use site below is guarded by 0 < c — audited site-by-site, no proof consumes the junk value. @audit:ok

The decreasing enumeration of the eigenvalues of the time-and-band limiting operator A = P_W ∘ Q_T ∘ P_W, listed with multiplicity and padded with 0.

Defined as the generalized inverse of the counting function prolateCount: λ n is the least threshold c > 0 above which A has at most n eigenvalues.

Scope: the unconditional headlines below (_nonneg, _le_one, _antitone, _tendsto_zero) are shape statements — each is satisfied by the constant-zero sequence, so none of them carries spectral content on its own. That is not a defect of the definition: for W ≤ 0 and for T ≤ 0 the operator genuinely collapses and the enumeration really is ≡ 0 (prolateEigenvalues_eq_zero_of_band_nonpos / prolateEigenvalues_eq_zero_of_time_nonpos), so a nondegeneracy input is needed to say more. prolateEigenvalues_zero_pos supplies it, ruling out the zero sequence for 0 < T, 0 < W; those two collapse lemmas are exactly what make its hypotheses tight.

Still open (a strictly larger obligation, not attempted here): λ n ≠ 0 for all n, which needs A to have infinite rank. Neither that nor the above is the Landau–Pollak–Slepian eigenvalue- concentration asymptotics (the ≈2WT-eigenvalue count) consumed downstream. @audit:ok

Every nonzero entry of the enumeration really is an eigenvalue of A. If it were not, the finitely many eigenvalues above c/2 would leave a gap around it, making the counting function constant across c — contradicting that the count jumps there by definition of the infimum.

The hypothesis is a non-degeneracy precondition, not the proof's core (granting it hands you nothing about eigenvalues; the gap argument below does the work). It is retained for content rather than necessity: at an entry with λ n = 0 the conclusion would assert only that 0 is an eigenvalue of A, which is no spectral information, so the hypothesis-free form would pin strictly less. At n = 0 it is discharged in-tree by prolateEigenvalues_zero_hasEigenvalue for 0 < T, 0 < W. @audit:ok

The indicator of the time window [0,T], as an element of L²(ℝ;ℂ). It is the witness that makes the eigenvalue enumeration non-vacuous: it lies in the time-limited subspace, and its spectrum is continuous with value T at the origin, hence survives the band cutoff. @audit:ok

The time-and-band limiting operator is nonzero whenever both the window and the band are nondegenerate. This is the non-vacuity input for the eigenvalue enumeration.

Both hypotheses are tight, and on structurally distinct grounds: at T = 0 the window collapses (timeLimitSubspace_eq_bot_of_nonpos, so Q = 0) and at W = 0 the band collapses (bandLimitSubspace_eq_bot_of_nonpos, so P = 0); either forces A = 0 (timeBandLimitingOp_eq_zero_of_time_nonpos / timeBandLimitingOp_eq_zero_of_band_nonpos). So neither can be relaxed to ≤. @audit:ok

The eigenvalue enumeration of the time-and-band limiting operator is non-vacuous: its leading entry is strictly positive whenever the window and the band are nondegenerate. This is what rules out the constant-zero sequence, which satisfies every shape headline on prolateEigenvalues. It bounds only the leading entry; λ n ≠ 0 for all n is a strictly larger, open obligation. @audit:ok

The leading entry of the enumeration is a genuine eigenvalue of A, discharging the non-degeneracy hypothesis of prolateEigenvalues_hasEigenvalue at n = 0. The discharge is not vacuous: the entry is strictly positive, so this exhibits a positive eigenvalue rather than the uninformative 0. @audit:ok

At a degenerate band the eigenvalue enumeration collapses to 0, so the 0 < W hypothesis of prolateEigenvalues_zero_pos cannot be relaxed to 0 ≤ W. @audit:ok

At a degenerate window the eigenvalue enumeration collapses to 0, so the 0 < T hypothesis of prolateEigenvalues_zero_pos cannot be relaxed to 0 ≤ T. @audit:ok