The L²(ℝ;ℂ) Hilbert space the operator acts on.

The closed subspace of L²(ℝ;ℂ) functions that vanish almost everywhere on a set S. It is a closed submodule: closedness comes from the fact that L² convergence has an almost-everywhere convergent subsequence, and an a.e.-limit of functions vanishing a.e. on S again vanishes a.e. on S.

Time-limited subspace: L² functions a.e.-supported in [0,T] (i.e. vanishing a.e. outside [0,T]). Closed.

Band-limited subspace: L² functions whose L²-Fourier transform is a.e.-supported in [-W,W] (i.e. vanishes a.e. on {ξ | W < |ξ|}). Closed, as the preimage of the closed subspace zeroOnLp {ξ | W < |ξ|} under the continuous Plancherel isometry.

The time-and-band limiting operator A = P_W ∘ Q_T ∘ P_W.

The time-and-band limiting operator is self-adjoint.

The time-and-band limiting operator is a positive operator.

The time-and-band limiting operator is a contraction: ‖A‖ ≤ 1.

The Hilbert–Schmidt kernel of the sinc integral operator C = Q_T ∘ P_W: 𝟙_[0,T](t) · 2W · sincN(2W(t − s)). The t-indicator encodes the time-limiting Q_T; the 2W sincN(2W·) factor is the ideal low-pass whose Fourier transform is 𝟙_[-W,W], i.e. the convolution kernel of the band-limiting P_W.

The sinc integral operator C = Q_T ∘ P_W (band-limit, then time-limit). A = P_W ∘ C.

The orthogonal projection onto zeroOnLp S acts, a.e., as multiplication by the indicator of Sᶜ. Proven via the uniqueness of the orthogonal projection: the candidate 𝟙_{Sᶜ}·g lies in the subspace, and the residual 𝟙_S·g is orthogonal to it. Both the time-limiting Q_T (S = [0,T]ᶜ) and the frequency-side multiplier (S = {|ξ| > W}, giving 𝟙_[-W,W]·𝓕f) are instances, so the projection-uniqueness argument is written once here. @audit:ok

The orthogonal projection Q_T onto the time-limited subspace acts, a.e., as multiplication by the indicator of [0,T]. The instance S = [0,T]ᶜ of zeroOnLp_starProjection_apply_ae. @audit:ok

Conjugating an orthogonal projection by a surjective linear isometry: the projection onto a comapped subspace is the projection onto the subspace, conjugated. Mathlib has the map form (LinearIsometry.map_starProjection); this is the comap form, which is what a Fourier-multiplier subspace such as bandLimitSubspace is literally defined by. @audit:ok

The band-limiting projection is the Fourier multiplier by 𝟙_[-W,W]: conjugate the projection onto zeroOnLp {ξ | W < |ξ|} by the Plancherel isometry. Immediate from starProjection_comap_linearIsometryEquiv and the definition of bandLimitSubspace. @audit:ok

The band-limiting projection is the Fourier multiplier by 𝟙_[-W,W], obtained by combining the conjugation identity bandLimitProj_eq_fourier_conj with the projection-uniqueness computation zeroOnLp_starProjection_apply_ae on the frequency side. This is the "half" of bandLimitProj_apply_ae that lives entirely inside the abstract projection API; the remaining half is the identification of the multiplier's action with sinc convolution, which needs the Fourier transform to be evaluated concretely. Note this half needs no sign condition on W: for W < 0 the interval [-W,W] is empty and both sides vanish, so the sign asymmetry is localized entirely in the passage from the multiplier 𝟙_[-W,W] to the kernel 2W sincN(2W·). @audit:ok

For a nonpositive time limit the time-limited subspace degenerates: the window [0,T] is empty (T < 0) or null (T = 0), so only the zero function is supported in it. Tightness half of the 0 < T hypothesis of prolateEigenvalues_zero_pos. @audit:ok

For a nonpositive band limit the band-limited subspace degenerates: the band [-W,W] is empty (W < 0) or null (W = 0), so only the zero function has an a.e.-vanishing Fourier transform outside it. Tightness half of the 0 < W hypothesis of prolateEigenvalues_zero_pos; it also discharges the degenerate band in the compactness headlines. @audit:ok

The frequency-side content of the band-limiting projection: the spectral cutoff 𝟙_[-W,W] · 𝓕f. By fourier_bandLimitProj_apply_ae this is a.e. the Fourier transform of P_W f; being an L² function cut down to a bounded interval it is moreover integrable, which is what lets the L¹ ∩ L² Fourier bridge evaluate P_W f pointwise.

The orthogonal projection P_W onto the band-limited subspace acts, a.e., as convolution with the ideal low-pass 2W sincN(2W·) (whose Fourier transform is 𝟙_[-W,W]). This is the abstract starProjection-of-a-comap-under-𝓕 ↔ concrete sinc-convolution identity, and it is what turns the operator C = Q_T ∘ P_W into an integral operator with the Hilbert–Schmidt kernel sincConvKernel.

The sign precondition 0 ≤ W is necessary, not cosmetic: sincN is even, so for W < 0 the stated kernel 2W sincN(2W·) is minus the ideal low-pass at |W|, while the left-hand side collapses to 0 (bandLimitSubspace_eq_bot_of_nonpos). Concretely at W = -1, f = 𝟙_[0,1], t = 1/2 the right-hand side is -∫_(-1)^(1) sincN ≈ -1.179 ≠ 0, so the unrestricted statement is false; 0 ≤ W is a precondition on the parameter, not a hypothesis carrying the proof.

The proof factors through the spectral cutoff bandLimitSpec W f = 𝟙_[-W,W]·𝓕f: the abstract half fourier_bandLimitProj_apply_ae identifies 𝓕(P_W f) with it, and since it is supported in a bounded interval it lies in L¹ ∩ L², so the Fourier bridge ShannonHartley.l2FourierInv_eq_fourierIntegralInv evaluates P_W f = 𝓕⁻¹(bandLimitSpec W f) pointwise as an integral (bandLimitProj_coeFn_ae_eq_fourierInv). That integral is then identified with the sinc convolution by Plancherel against the spectral boxcar, whose inverse transform is already known to be a shifted sinc (ShannonHartley.fourier_shiftSinc_toLp). The degenerate W = 0 band is a null set, where both sides vanish. @audit:ok

Complex conjugation on L²(ℝ;ℂ) as a conjugate-linear map. Mathlib equips Lp with a bare Star instance only (no StarAddMonoid / StarModule), so the additivity and conjugate-homogeneity that bundle it into a semilinear map are supplied here by star_add_Lp / star_smul_Lp.

A = P_W ∘ Q_T ∘ P_W commutes with complex conjugation: each factor does, since the time window [0,T] and the symmetric band [-W,W] are conjugation-invariant. Stated for all W; for W < 0 the band is empty and both sides collapse to 0. sorryAx-free, no hypotheses (no hW) so the statement is universal, not weakened. @audit:ok

The normalized sinc is square-integrable on ℝ. The reusable crux for the kernel-L² bound: its Lebesgue L²-membership follows from the elementary majorant sincN(x)² ≤ 2/(1 + x²) (|sincN| ≤ 1 near 0, sincN(x)² = sin²(πx)/(πx)² ≤ 1/(πx)² away from it) against the integrable 2/(1 + x²). Mathlib's Real.integrable_sinc is finite-measure-only, so the Lebesgue L² fact is built here. @audit:ok

sincConvKernel is square-integrable on ℝ × ℝ: the t-indicator confines the mass to [0,T] and the inner mass ∫_ℝ (2W sincN(2W(t−s)))² ds is a finite constant C (independent of t, by translation invariance of Lebesgue measure), so ‖k‖₂² ≤ C · vol[0,T] < ∞. The finite L² mass of the ideal low-pass 2W sincN(2W·) is obtained by rescaling the 1-D crux sincN ∈ L² (sincN_memLp_two) through integrable_comp_mul_left_iff, and the 2-D lift is a Tonelli (lintegral_prod_le) + lintegral_sub_left_eq_self computation. Hypothesis-free in T and W: the degenerate T < 0 (empty [0,T], zero mass) and 2W = 0 (zero kernel) cases are both covered. @audit:ok

The L²(ℝ × ℝ; ℂ) space of Hilbert–Schmidt kernels.

The integral operator attached to a kernel, at the level of raw functions: f ↦ (t ↦ ∫ k(t,s) f(s) ds).

The integral operator of a kernel, as a linear map on L²(ℝ;ℂ).

The kernel-to-operator map, as a bilinear map.

The kernel-to-operator map κ ↦ (f ↦ ∫ κ(·,s) f(s) ds), as a continuous linear map. Its continuity is exactly the Hilbert–Schmidt bound ‖l2KernelOp κ‖ ≤ ‖κ‖. @audit:ok

A rectangle kernel c · 𝟙_{A×B} induces a rank-one operator, hence a compact one. The degenerate branch (vol A * vol B = 0, which by 0 * ∞ = 0 in ℝ≥0∞ also covers a null side paired with an infinite one) is not an escape: Measure.prod_prod makes the rectangle product-null, so the kernel is the zero element of L²(ℝ × ℝ) and the induced operator really is 0. @audit:ok

The exhausting family of squares [-R,R] × [-R,R] in ℝ × ℝ. Each is a rectangle of finite measure, and they increase to the whole plane; intersecting with them reduces the kernel density argument to sets of finite measure.

An integral operator on L²(ℝ;ℂ) whose kernel is L² on ℝ × ℝ is a compact operator; it is realized a.e. as f ↦ ∫ k(·,s) f(s) ds. Built via the reusable l2KernelOp Hilbert–Schmidt machinery above (Mathlib has no Hilbert–Schmidt API). Stated existentially so the operator object is constructed together with its compactness rather than assumed; the a.e.-representation clause pins Op uniquely (an Lp element is an a.e. class), so the existential is not weakened by it. @audit:ok

The sinc integral operator C = Q_T ∘ P_W acts a.e. as the integral operator of sincConvKernel. Composition of timeLimitProj_apply_ae and bandLimitProj_apply_ae. The 0 ≤ W hypothesis is inherited from the latter as a parameter precondition and is discharged by the caller's case split. @audit:ok

The sinc integral operator C = Q_T ∘ P_W is compact. Reduction: the operator built by l2KernelOperator_isCompact for sincConvKernel coincides with C (both have the same a.e. representative, hence are equal in Lp). No sign restriction on W: for W < 0 the kernel representation is unavailable (and false), but there P_W = 0, so C = 0 is compact outright. @audit:ok

The time-and-band limiting operator is compact: A = P_W ∘ C with C = Q_T ∘ P_W compact (the sinc integral operator) and P_W bounded, so A is compact by clm_comp.

Unconditional: the signature carries no hypothesis on T or W, and both degenerate parameter ranges are discharged by real proofs rather than assumed away — W < 0 via bandLimitSubspace_eq_bot_of_nonpos (P_W = 0, so C = 0), T < 0 via the empty [0,T] (Q_T = 0), and W = 0 inside bandLimitProj_apply_ae as a null-band case. @audit:ok