The reproducing kernel of the band-limited subspace at time t: the ideal low-pass 2W sincN(2W(t − ·)), whose Fourier transform is the spectral boxcar 𝟙_[-W,W] e^{-2πi t ·}. It is the integral kernel of P_W, so pairing against it evaluates a band-limited function at t.

The 2W factor is not a free constant: bandLimitProj_apply_ae pins it against the Fourier definition of bandLimitSubspace, so a wrong gain fails to compile rather than rescaling the bound below. @audit:ok

The kernel is a constant multiple of the shifted, dilated sinc sincN((· − t)/Δ) at Δ = 1/(2W), whose L² membership is ShannonHartley.shiftSinc_memLp. @audit:ok

The reproducing kernel at time t, as an element of L²(ℝ;ℂ). @audit:ok

The reproducing property of the band-limited subspace: (P_W f)(t) = ⟪k_t, f⟫ for a.e. t, with k_t = bandKernelLp W t the ideal low-pass centered at t. This is bandLimitProj_apply_ae read as an L² pairing; the kernel is real-valued, so the conjugation in the (conjugate-linear-in-the-first-slot) inner product is invisible. @audit:ok

The quadratic form of A is the energy of P_W f observed through the window [0,T]: ⟪A f, f⟫ = ∫_[0,T] |⟪k_t, f⟫|² dt. Self-adjointness of P_W moves one copy across the pairing, and timeLimitProj_apply_ae turns Q_T into multiplication by 𝟙_[0,T]. @audit:ok

The trace of the time-and-band limiting operator along any finite orthonormal family is at most 2WT.

The quadratic form ⟪A eᵢ, eᵢ⟫ = ∫_[0,T] |⟪k_t, eᵢ⟫|² dt (inner_timeBandLimitingOp_self_eq) turns the trace into an integral of a finite sum, so the sum and the integral commute without any Fubini; Bessel's inequality then caps the integrand by the constant ‖k_t‖² = 2W (bandKernelLp_norm_sq), and the window [0,T] supplies the factor T. No trace-class or Schatten theory is involved — only a finite orthonormal family — so Mathlib's lack of Schatten API does not block this bound.

Scope: this is the trace bound, not the Landau–Pollak–Slepian degrees-of-freedom count. It is the same Bessel argument that already closes contAwgnMaxMessages_bddAbove wall-free, and like that bound it yields the crude constant only. It does not bear on the Landau–Pollak–Slepian eigenvalue concentration (≈2WT eigenvalues near 1, the rest near 0); Bessel is one-directional and cannot reach it. @audit:ok

An orthonormal family in a separable inner-product space is countable.

Distinct members sit at distance √2, so the open balls of radius 1/2 around them are pairwise disjoint, and a separable space admits only countably many pairwise-disjoint nonempty open sets (Pairwise.countable_of_isOpen_disjoint). Mathlib has no such lemma (loogle Orthonormal, Countable = Found 0), so it is built here; it is what lets tsum_inner_timeBandLimitingOp_eq derive the countability its Tonelli step needs instead of assuming it. @audit:ok

The trace of the time-and-band limiting operator along any complete orthonormal basis is exactly 2WT.

This upgrades the Bessel inequality sum_inner_timeBandLimitingOp_le to a Parseval equality. The quadratic form ⟪A bᵢ, bᵢ⟫ = ∫_[0,T] |⟪k_t, bᵢ⟫|² dt (inner_timeBandLimitingOp_self_eq) makes the trace a sum of integrals of nonnegative terms, so Tonelli (lintegral_tsum, over ℝ≥0∞) exchanges ∑' and ∫ with no joint-integrability side condition; completeness of the basis then replaces Bessel by Parseval (hasSum_norm_inner_bandKernelLp_sq), pinning the integrand to exactly ‖k_t‖² = 2W (bandKernelLp_norm_sq), and the window [0,T] supplies the factor T.

No spectral theorem and no trace-class theory are used: Mathlib's lack of Schatten/Hilbert–Schmidt API (real, and confirmed) does not block this identity. Countability of the index — the Tonelli step's only structural need — is derived from separability of L²(ℝ;ℂ) via orthonormal_countable, not assumed. exists_hilbertBasis_tsum_inner_timeBandLimitingOp_eq witnesses in-tree that such a basis exists, so the statement is not vacuous.

Scope: this is an exact first moment ∑ λₙ = 2WT, which is not the Landau–Pollak–Slepian concentration #{n | λₙ > c} = 2WT + O(log WT), and the first moment does not reach it in either direction. Upward it feeds only Markov (prolateCount_mul_le), which uses just the ≤ half and overcounts by 1/c; the exactness buys nothing there. Downward it is strictly insufficient: a spectrum with ∑ λₙ = 2WT and every λₙ ≤ c has #{λₙ > c} = 0, so no lower bound on the count follows from the first moment alone. Splitting the sum gives #{λₙ > c} ≥ 2WT − ∑_{λₙ ≤ c} λₙ, whose tail term is controlled only by the second moment ∑ λₙ(1 − λₙ) = tr A − tr A². That second moment — not this identity — remains the blocker. @audit:ok

Non-vacuity of tsum_inner_timeBandLimitingOp_eq, machine-checked rather than asserted: a Hilbert basis of L²(ℝ;ℂ) exists (exists_hilbertBasis), so the trace identity is a statement about a real object and not an empty quantification over an uninhabited hypothesis. @audit:ok

Complex conjugation preserves the span of the high eigenspaces. The operator A commutes with star (timeBandLimitingOp_star_comm) and its eigenvalues are real, so each eigenspace above c is star-invariant; the span inherits it. This is the ℂ/ℝ bridge that lets the achievability path choose real-valued prolate eigenfunctions — it proves the span is star-invariant, not that any individual eigenfunction is real (the latter is the downstream real-basis extraction, not claimed here). sorryAx-free, the hv hypothesis is the antecedent of a closure property (not load-bearing), and the prose does not overclaim. @audit:ok

A restricted to the orthogonal complement of the span of the eigenspaces above c.

This is the restriction of A, not a disguised 0: the rfl step in inner_timeBandLimitingOp_le_of_mem_orthogonal proves (prolateRestrict T W c ⟨v, hv⟩ : E) = timeBandLimitingOp T W v definitionally, which no zero map could satisfy for a nonzero A (timeBandLimitingOp_ne_zero). @audit:ok

The restriction of A to Vᗮ is a contraction by c: ‖S‖ ≤ c.

hc : 0 < c is regularity, not load-bearing: it is consumed only to place the spectral point 0 below the bound and to invert ENNReal.ofReal, never to supply spectral content. The route was machine-confirmed by walking the transitive constant graph rather than read off the prose — ContinuousLinearMap.spectralRadius_eq_nnnorm (Rayleigh) and IsCompactOperator.hasEigenvalue_iff_mem_spectrum are both consumed, and ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot is not. @audit:ok

The spectral gap below c: on the orthogonal complement of the span of every eigenspace of A with eigenvalue exceeding c, the Rayleigh quotient of A is at most c.

This is the qualitative half of the eigenvalue count: together with the exact trace tsum_inner_timeBandLimitingOp_eq (tr A = 2WT) and the second-moment bound tsum_inner_sub_norm_sq_timeBandLimitingOp_le (tr A − tr A² = O(log WT)), it is what lets a Chebyshev split localize the spectrum around the cliff at c.

The proof needs no eigenbasis. prolateEigenspaceSup_invariant and symmetry make Vᗮ invariant, so A restricts to a compact self-adjoint operator S there; every eigenvalue of S is an eigenvalue of A lying in [0, c] (above c its eigenvector would land in V ⊓ Vᗮ = ⊥), and for a compact self-adjoint operator the norm is the spectral radius, so ‖S‖ ≤ c. Cauchy-Schwarz then gives the Rayleigh bound. In particular this route does not construct a complete orthonormal eigenbasis of A (that route is tsum_prolateEigenvalues_eq, taken separately).

Unconditional in T and W: compactness, symmetry and positivity of A all hold for every parameter value, so no window or band nondegeneracy is assumed. Only 0 < c is needed, and only to place the point 0 of the spectrum below the bound.

No hypothesis carries the core. The bundle is hc : 0 < c (positivity of a free threshold) and hv : v ∈ Vᗮ (membership in a submodule defined outright, not asserted). Granting both hands over no spectral fact: the substance — that compactness collapses the spectrum onto eigenvalues, and self-adjointness turns the spectral radius back into the norm — is all discharged in the body. The specific risk was an input amounting to "A has a complete eigenbasis" or "the spectrum below c is discrete"; no such hypothesis is present, and the transitive constant graph confirms mechanically that orthogonalComplement_iSup_eigenspaces_eq_bot, HilbertBasis.mkOfOrthogonalEqBot and finite_dimensional_eigenspace are all consumed zero times: the claim to need no eigenbasis is machine-confirmed, not asserted.

No redundant hypotheses. The statement drops hT : 0 ≤ T and hW : 0 < W as unused — strictly stronger, nothing added.

Sufficiency, re-derived. Symmetry forces every eigenvalue real (conj_eigenvalue_eq_self), so spanning only the real eigenvalues above c leaves no complex eigenvalue hiding in Vᗮ — the gap this shape could plausibly have had, and it is closed. Two structurally different degenerate boundaries were checked, not just one: at T ≤ 0 the operator collapses (A = 0, V = ⊥, Vᗮ = ⊤) and the claim reads 0 ≤ c‖v‖², true; at c ≥ 1 we again get V = ⊥ (prolateEigenvalueSet_one_eq_empty) and the claim reduces to ‖A‖ ≤ 1, true. The invariant the hypotheses pin — v ⊥ every eigenspace above c — is exactly the granularity the conclusion needs, not coarser: it is what forces spectrum (A|Vᗮ) ⊆ [0, c].

Not vacuous where it matters. For 0 < c, V is finite-dimensional (prolateEigenspaceSup_finiteDimensional) while E = L²(ℝ;ℂ) is not, so Vᗮ ≠ ⊥ and the bound speaks about real vectors. Unlike its siblings in this file the non-vacuity is argued, not machine-checked by an in-tree witness lemma; nothing downstream currently depends on that witness. @audit:ok

V-side operator lower bound: on the span V = prolateEigenspaceSup T W c of the eigenspaces above c, the Rayleigh quotient of A is at least c. This is the matched pair to inner_timeBandLimitingOp_le_of_mem_orthogonal, which caps it by c on Vᗮ.

V is finite-dimensional and A-invariant, so the finite-dimensional spectral theorem supplies an orthonormal eigenbasis b of V with every eigenvalue exceeding c. Expanding v along b, ⟪A v, v⟫ = ∑ᵢ νᵢ ‖⟪bᵢ, v⟫‖² ≥ c ∑ᵢ ‖⟪bᵢ, v⟫‖² = c ‖v‖² by Parseval, since every νᵢ > c.

sorryAx-free (#print axioms = [propext, Classical.choice, Quot.sound]). Both hypotheses are preconditions, not core: hc : 0 < c gives finite-dimensionality of V (so the spectral theorem applies) and hv : v ∈ V scopes the claim; neither is := h circular, a :True slot, or a load-bearing bundle. The body proves the stated bound c‖v‖² ≤ Re⟪Av,v⟫, not a weaker 0-bound: the hνgt block earns νᵢ > c from the orthogonality argument (an eigenvector for an eigenvalue ≤ c would be ⊥ to every eigenspace above c, hence to V ∋ bᵢ, hence zero, contradicting unit norm), then Parseval closes it. Not vacuous where it bites (V non-trivial below the top eigenvalue via exists_unit_eigenvector); at the boundaries it degenerates to 0 ≤ c‖v‖², true. @audit:ok

Count domination in the converse min-max direction: any subspace S on which the Rayleigh quotient of A = timeBandLimitingOp T W strictly exceeds c has dimension at most prolateCount T W c: the number of "high-gain" directions is capped by the number of prolate eigenvalues above c. Finite-dimensional min-max half of Cauchy interlacing; converse companion to the achievability count.

sorryAx-free (#print axioms = [propext, Classical.choice, Quot.sound]; its crux inner_timeBandLimitingOp_le_of_mem_orthogonal re-verified sorryAx-free too). The hypothesis hS is a min-max precondition — it constrains only the Rayleigh-quotient form c‖x‖² < Re⟪Ax,x⟫ on S and names no count/eigenvalue/prolate object, so it does not bundle the conclusion finrank S ≤ prolateCount. The body does real work: the strict form on S collides with the ≤ c bound on Vᗮ (crux) to force S ∩ Vᗮ = {0}, whence orthogonal projection injects S ↪ V and finrank S ≤ finrank V = prolateCount. Not vacuous (a ≤ on finrank S, not 0 ≤ _ or finrank ⊥). @audit:ok

Markov bound on the eigenvalue counting function: at most 2WT/c eigenvalues of the time-and-band limiting operator exceed c.

The span prolateEigenspaceSup T W c of the eigenspaces above c is A-invariant and finite-dimensional, so the finite-dimensional spectral theorem supplies an orthonormal eigenbasis of it; every one of its eigenvalues exceeds c (an eigenvector for an eigenvalue ≤ c would be orthogonal to every eigenspace above c, hence to the span containing it, hence zero). Feeding that basis to sum_inner_timeBandLimitingOp_le gives c · #{λ > c} ≤ ∑ λᵢ ≤ 2WT.

Scope: read as a count this says #{λ > c} ≤ 2WT/c, which overcounts by the factor 1/c and has no vanishing relative error. It is therefore weaker than the sharp upper half #{λ > c} ≤ 2WT + O(log WT), and weaker still than the two-sided Landau–Pollak–Slepian concentration. Neither downstream consumer is unblocked by it: contAwgn_ge_shannonHartley needs the lower half, and contAwgn_eq_shannonHartley, being an equality, needs both halves sharply.

Non-vacuity is machine-checked rather than assumed: for 0 < T, 0 < W, exists_pos_hasEigenvalue yields an eigenvalue μ > 0, so prolateCount T W (μ/2) ≥ 1 and the bound bites (μ/2 ≤ 2WT) instead of holding by 0 ≤ 2WT. @audit:ok @audit:retract-candidate(superseded by prolateCount_le for the family's purpose; 0 consumers, machine-checked via scripts/dep_consumers.sh. This is asymptotic supersession, not pointwise — 2WT/c is strictly tighter than 2WT + (2+log(1+2WT))/c for small WT (e.g. 2WT ≤ 8 at c = 1/2), so the two are incomparable as bounds. What makes it retractable is that the family's figure of merit is the T → ∞ density, where this bound gives 2W/c and prolateCount_le gives 2W.)

Every eigenspace of the compact operator A = timeBandLimitingOp T W is complete: it is the kernel of the continuous map A − μ•1, hence closed in the complete space E. Uniform in μ (both the finite-dimensional eigenspaces for μ ≠ 0 and the possibly infinite-dimensional kernel), which is what lets the per-eigenspace Hilbert bases be chosen without a dimension case split.

A complete orthonormal eigenbasis of A = timeBandLimitingOp T W exists. The operator is compact and self-adjoint, so its eigenspaces are total (orthogonalComplement_iSup_eigenspaces_eq_bot). Collating a Hilbert basis of each eigenspace (exists_hilbertBasis, uniform in μ) over Σ μ : ℂ, … and gluing by mkOfOrthogonalEqBot yields a complete orthonormal eigenbasis of E, with real nonnegative eigenvalues, whose vectors with eigenvalue above c span the high eigenspace prolateEigenspaceSup T W c.

No hypotheses; the whole construction is in the body. All three conjuncts are proven — the eigen-relation and nonnegativity pointwise, and the span identity by a real two-sided le_antisymm (not :True). The third conjunct is non-vacuous: were {i | c < lam i} empty for all c > 0, nonnegativity would force lam ≡ 0, contradicting tsum_eigen_eq_two_mul's ∑ lam = 2WT ≠ 0 for 0 < W, 0 < T. sorryAx-free (#print axioms = [propext, Classical.choice, Quot.sound]). @audit:ok

The eigenvalue sum along a complete eigenbasis of A equals 2WT, obtained by feeding the eigenbasis to tsum_inner_timeBandLimitingOp_eq and simplifying each Rayleigh quotient ⟪A bᵢ, bᵢ⟫.re to its eigenvalue lam i.

For t > 0, only finitely many eigenbasis vectors have eigenvalue above t: they are orthonormal (hence linearly independent) and lie in the finite-dimensional high eigenspace prolateEigenspaceSup T W t.

The super-level count of the eigenbasis eigenvalues equals prolateCount: the vectors with eigenvalue above t form an orthonormal basis of prolateEigenspaceSup T W t, so their number is its finrank.

For t > 0, the decreasing enumeration exceeds t exactly on an initial segment {0, …, prolateCount T W t − 1}. This is the generalized-inverse duality t < prolateEigenvalues T W n ↔ n < prolateCount T W t, packaged as a set identity. The ← direction uses the finiteness of the eigenvalue set above t to produce a spectral gap just above t, so the counting function is locally constant there and the infimum defining prolateEigenvalues clears t strictly.

The multiplicity bridge: the eigenvalue sum along the eigenbasis equals the sum over the decreasing enumeration prolateEigenvalues, since both nonnegative families share the super-level counts #{· > c} = prolateCount T W c (the eigenbasis vectors above c span prolateEigenspaceSup T W c, whose finrank is prolateCount — ncard_setOf_lt_lam; the enumeration exceeds c on the initial segment {0, …, prolateCount T W c − 1} — setOf_lt_prolateEigenvalues_eq_Iio), transported through the layer-cake identity lintegral_eq_lintegral_meas_lt: both ℝ≥0∞ sums equal ∫⁻ t ∈ Ioi 0, prolateCount T W t. Summability of both families (summable_of_sum_le from the Bessel bound, then ENNReal.summable_toReal) converts the ℝ≥0∞ equality back to ℝ.

heig/hnn/hspan are structural preconditions describing an abstract eigenbasis, not the conclusion in disguise — the multiplicity core (layer-cake lintegral_eq_lintegral_meas_lt, Bessel summability, the Measure.count distribution functions) is carried by the body. They are discharged by feeding exists_eigen_hilbertBasis's output at the headline tsum_prolateEigenvalues_eq, which therefore assumes none of them (no load-bearing bundle). sorryAx-free (#print axioms = [propext, Classical.choice, Quot.sound]). @audit:ok

The trace identity tsum_inner_timeBandLimitingOp_eq, transported onto the decreasing eigenvalue enumeration: ∑ₙ λₙ = 2WT (the exact first spectral moment of A = timeBandLimitingOp).

sorryAx-free, and independent of the Landau–Pollak–Slepian concentration. It composes three pieces, each proved from assets already in Mathlib / this file:

1. exists_eigen_hilbertBasis — a complete orthonormal eigenbasis of A. The compact self-adjoint spectral theorem (ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot: the eigenspaces are total) glues per-eigenspace Hilbert bases (exists_hilbertBasis, uniform in μ) into one orthonormal family via HilbertBasis.mkOfOrthogonalEqBot, with real nonnegative eigenvalues whose above-c vectors span prolateEigenspaceSup T W c.
2. tsum_eigen_eq_two_mul — feeding that eigenbasis to the trace identity gives ∑ λ = 2WT.
3. tsum_eigen_eq_tsum_prolateEigenvalues — the multiplicity bridge to prolateEigenvalues, the generalized inverse sInf {c > 0 | prolateCount T W c ≤ n} of the counting function: both nonnegative families share the super-level counts prolateCount T W t, so a layer-cake identity equates their sums.

None of this is the Landau-Pollak-Slepian asymptotics in WT; it is c-by-c structure for a compact positive operator. This exact first moment is off the Shannon-Hartley converse path (a bonus: the converse lands via count domination bandGramReal_high_count_le, not this identity).

Unconditional — the body obtains the eigenbasis data heig/hnn/hspan from the hypothesis-free exists_eigen_hilbertBasis, so it discharges (does not assume) the eigenbasis preconditions. The only hypotheses hT : 0 ≤ T, hW : 0 < W are domain regularity (matching the already-audited tsum_inner_timeBandLimitingOp_eq), fixing the nonnegative value 2WT. No load-bearing hypothesis, no circularity. sorryAx-free (#print axioms = [propext, Classical.choice, Quot.sound]). @audit:ok