The polarized form behind A = P_W Q_T P_W being positive: ⟪A x, y⟫ = ⟪Q_T P_W x, Q_T P_W y⟫.

A = C* C for C = Q_T ∘ P_W, so the sesquilinear form of A is the inner product pulled back along C. This is the diagonal identity inside norm_timeBandLimitingOp_sq_le_inner, polarized; it is what makes Cauchy-Schwarz available for the form of A without a positive square root. @audit:ok

Cauchy-Schwarz for the positive form of A: |⟪A x, y⟫|² ≤ ⟪A x, x⟫ ⟪A y, y⟫.

Mathlib has Cauchy-Schwarz for an inner product (norm_inner_le_norm) but not for the semi-inner product of a general positive operator, which would need a positive square root. Here the square root is unnecessary: A is concretely C* C, so its form is an inner product pulled back along C and Mathlib's Cauchy-Schwarz applies verbatim. @audit:ok

The operator inequality A² ≤ c·A on Vᗮ, in basis-free form: for v orthogonal to every eigenspace above c, ‖A v‖² ≤ c ⟪A v, v⟫.

This sharpens norm_timeBandLimitingOp_sq_le_inner (A² ≤ A, valid everywhere) by the spectral gap, and it is what turns the second-moment deficit on Vᗮ into a bound on the Vᗮ trace in le_prolateCount.

The proof needs no positive square root and no restricted operator. Cauchy-Schwarz for the form of A (norm_inner_timeBandLimitingOp_sq_le), tested at x = v and y = A v, gives ‖A v‖⁴ ≤ ⟪A v, v⟫ ⟪A(A v), A v⟫; since Vᗮ is A-invariant, A v is again in Vᗮ, so the spectral gap inner_timeBandLimitingOp_le_of_mem_orthogonal caps the second factor by c ‖A v‖², and dividing by ‖A v‖² finishes.

hc : 0 < c and hv are regularity/scoping, not load-bearing: the operator inequality is derived from Cauchy-Schwarz + the gap lemma, not assumed. sorryAx-free. @audit:ok

An orthonormal eigenbasis of the finite-dimensional V = prolateEigenspaceSup T W c, indexed by Fin (prolateCount T W c), with every eigenvalue exceeding c, spanning V back in E.

This is the finite-dimensional spectral theorem applied to A|_V; it needs no complete eigenbasis of A on E.

The index type is Fin (prolateCount T W c) definitionally (prolateCount is the finrank of V), which is why no separate multiplicity bridge is needed to match the count.

The definitional claim is machine-confirmed, not prose: the body's have hn : Module.finrank ℂ (prolateEigenspaceSup T W c) = d := rfl type-checks, and prolateCount T W c := Module.finrank ℂ (prolateEigenspaceSup T W c) verbatim. sorryAx-free. @audit:ok

A Hilbert basis of E adapted to E = V ⊕ Vᗮ: its V half is an eigenbasis of A with every eigenvalue exceeding c, and its Vᗮ half lies in Vᗮ.

The trace identities tsum_inner_timeBandLimitingOp_eq and tsum_inner_sub_norm_sq_timeBandLimitingOp_le hold along an arbitrary Hilbert basis; feeding them this one is what splits tr A and tr A − tr A² along the spectral cliff at c.

The Vᗮ half is an arbitrary Hilbert basis of Vᗮ (exists_hilbertBasis, i.e. Zorn) and is not an eigenbasis: no complete eigenbasis of A is constructed anywhere. Completeness of the glued family comes from V being spanned by the finite eigenbasis and Vᗮ by its own Hilbert basis, so a vector orthogonal to all of them lies in Vᗮ with vanishing Vᗮ-coordinates, hence is zero.

The "no complete eigenbasis of A on E" claim is machine-confirmed by a constant-graph walk (validated against a positive control): this decl's closure does not contain ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot, the infinite-dimensional totality lemma. It does contain LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot and IsCompactOperator — both via the finite-dimensional spectral theorem for A|_V and prolateEigenspaceSup_finiteDimensional, i.e. about V, not about a complete eigenbasis on E. sorryAx-free. @audit:ok

The real form of V = prolateEigenspaceSup T W c: its star-fixed elements, viewed as an ℝ-subspace of E. Since V is conjugation-invariant (star_mem_prolateEigenspaceSup), it is the complexification of this real form, and a real orthonormal basis of the real form is a ℂ-orthonormal basis of V whose members are star-fixed (a.e. real-valued).

The canonical ℝ-linear injection of the real form into ↥V, used to transport finite-dimensionality of V over ℝ to its real form.

A star-fixed (a.e. real-valued) ℂ-orthonormal basis of V = prolateEigenspaceSup T W c.

V is finite-dimensional (prolateEigenspaceSup_finiteDimensional) and closed under complex conjugation (star_mem_prolateEigenspaceSup), so it is the complexification of its real form V_ℝ = {v ∈ V | star v = v} (realForm). A standard real orthonormal basis of V_ℝ (stdOrthonormalBasis) is ℂ-orthonormal — its inner products are real for star-fixed vectors (inner_complex_eq_real_of_star_fixed) — and ℂ-spans V: every v ∈ V decomposes as (v + star v)/2 + I·(I/2)·(star v − v), two star-fixed summands. Counting shows the basis has finrank ℂ V = prolateCount T W c members, so it reindexes onto Fin (prolateCount T W c). This is the ℂ/ℝ bridge the achievability path needs: it lets the prolate eigenfunctions be chosen real-valued.

This exports star-fixed elements of E = Lp ℂ 2 volume (whose a.e. representative is real-valued); turning them into the ℝ → ℝ matched-filter test functions the ContAwgnCode consumer wants (with [0,T] support / band-limit) is a further step, not established here. Also note u is an orthonormal basis of V (a sum of eigenspaces over {μ > c}), not per se an A-eigenbasis: its members span V but need not be single-eigenvalue eigenfunctions, so a downstream ψᵢ/√μᵢ normalization requires first refining u into an eigenbasis — the same real-form bridge applied eigenspace-by-eigenspace — which this theorem does not perform.

#print axioms = [propext, Classical.choice, Quot.sound], sorryAx-free. Signature is a plain existence: hc : 0 < c is a regularity precondition (it makes V finite-dimensional via prolateEigenspaceSup_finiteDimensional, otherwise prolateCount is a junk 0), with no := h circularity, no :True slot, no load-bearing hypothesis. Body proves all three conjuncts (ℂ-orthonormal, star-fixed, span = V); the count is derived (finrank_span_eq_card on the ℂ-independent star-fixed family, = prolateCount), and the prolateCount = 0 case is the empty family with span ⊥ = V, not a degenerate trick. No overclaim on ℝ → ℝ / [0,T]-support. @audit:ok

Upper half of the eigenvalue count concentration: with D := 2 + log(1 + 2WT), the number of eigenvalues of A exceeding c is at most 2WT + D/c, for every free threshold 0 < c.

Together with le_prolateCount this is the Landau-Pollak-Slepian concentration #{λ > c} = 2WT ± O(log WT). The threshold c is a free variable, not fixed at 1/2: the downstream converse needs c → 0 and the achievability needs c → 1, so a fixed c closes neither.

Not the Markov bound. prolateCount_mul_le gives #{λ > c} ≤ 2WT/c, which overcounts by 1/c with no vanishing relative error. This bound has relative error → 0 as WT → ∞ for fixed c, which is what the exact constant in Shannon-Hartley needs. (Neither dominates pointwise: for small WT the Markov bound is numerically tighter. The content here is the asymptotic shape.)

Mechanism: on V the adapted basis of exists_hilbertBasis_prolateSplit is an eigenbasis, so the exact trace tr A = 2WT caps ∑_V λᵢ (the rest of the trace being nonnegative) and the second-moment bound tr A − tr A² ≤ D caps ∑_V λᵢ(1 − λᵢ) (the deficit being nonnegative termwise, by A² ≤ A). Since λᵢ > c, ∑_V (1 − λᵢ) ≤ (1/c) ∑_V λᵢ(1 − λᵢ) ≤ D/c, and n − ∑_V λᵢ ≤ D/c gives the claim. No eigenbasis of A on E is used; the spectral gap on Vᗮ is not used either (machine-checked: this half's constant closure contains neither inner_timeBandLimitingOp_le_of_mem_orthogonal nor ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot).

Degenerate boundaries: at T = 0 both sides collapse to 0 ≤ D/c; at c ≥ 1 the count is 0 (prolateCount_one_eq_zero and antitonicity) and the bound is slack.

All four hypotheses are regularity on scalars; nothing of the form "A has a complete eigenbasis" / "S² ≤ cS" / "an adapted basis exists" is assumed — each is derived (exists_hilbertBasis_prolateSplit, norm_timeBandLimitingOp_sq_le_of_mem_orthogonal). sorryAx-free. The consumers' figure of merit is the DOF density n(T)/T as T → ∞, where Markov gives 2W/c (wrong constant, diverging as c → 0) and this bound gives exactly 2W for every fixed c > 0. The pointwise incomparability at small WT is real but is not the figure of merit. @audit:ok

Lower half of the eigenvalue count concentration: with D := 2 + log(1 + 2WT), the number of eigenvalues of A exceeding c is at least 2WT − D/(1 − c), for every free 0 < c < 1.

The companion of prolateCount_le. This is the half no trace bound alone can reach: tr A = 2WT is a coarse scalar and does not by itself forbid a flat spectrum with every λ ≤ c and count 0. What rules that out is the second moment.

Mechanism: split the exact trace along the adapted basis of exists_hilbertBasis_prolateSplit, 2WT = ∑_V λᵢ + ∑_{Vᗮ} aⱼ. Each λᵢ ≤ 1 (contraction), so ∑_V λᵢ ≤ n. On Vᗮ the sharpened operator inequality A² ≤ cA (norm_timeBandLimitingOp_sq_le_of_mem_orthogonal) makes each deficit aⱼ − ‖A bⱼ‖² ≥ (1 − c) aⱼ, and the second-moment bound tr A − tr A² ≤ D caps the sum of deficits, so ∑_{Vᗮ} aⱼ ≤ D/(1 − c).

hc1 : c < 1 is a precondition, not padding: at c = 1 Lean's x/0 = 0 convention would read the claim as 2WT ≤ #{λ > 1} = 0 (prolateCount_one_eq_zero), which is false for WT > 0. As c ↑ 1 the bound degrades to −∞, consistently. At T = 0 it reads −D/(1−c) ≤ 0, true. The bound has content rather than holding vacuously: at c = 1/2 it bites once 2WT ≳ 8.

sorryAx-free; hypotheses are regularity only. Two claims above were machine-checked rather than accepted: (a) hc1 is load-bearing as a precondition — the c = 1 instance of this conclusion was proved false at T = W = 1 (via prolateCount_one_eq_zero + x/0 = 0), so dropping hc1 would make the statement false, not merely weaker; (b) the 2WT ≳ 8 crossover is accurate (numerically, the bound turns positive at 2WT ≈ 8.5). Markov (prolateCount_mul_le) cannot substitute here at any c: it is an upper bound only and supplies no lower half at all. Density n(T)/T → 2W for every fixed c < 1, which is what the achievability consumer's iterated limit (T → ∞, then c → 1) needs. @audit:ok

Members of V = prolateEigenspaceSup T W c are band-limited: V ≤ bandLimitSubspace W.

An eigenvector for eigenvalue μ > c > 0 satisfies A v = μ v; since A = P_W ∘ Q_T ∘ P_W has range inside bandLimitSubspace W, so does μ v, and μ ≠ 0 gives v ∈ bandLimitSubspace W. The span of these eigenspaces stays inside the closed subspace bandLimitSubspace W.

Time-window energy concentration: for v ∈ V = prolateEigenspaceSup T W c and 0 < c, the time-limited energy retains at least the fraction c of the total energy: c ‖v‖² ≤ ‖Q_T v‖², where Q_T = (timeLimitSubspace T).starProjection.

This is the prolate-spheroidal concentration statement the achievability receiver relies on. It comes straight from le_inner_timeBandLimitingOp_of_mem (the Rayleigh lower bound c‖v‖² ≤ ⟪A v, v⟫) once the polarization identity inner_timeBandLimitingOp_eq_inner_timeLimit_bandLimit collapses ⟪A v, v⟫ to ‖Q_T P_W v‖² and prolateEigenspaceSup_le_bandLimitSubspace removes P_W on V.

The time-limiting projection Q_T is injective on V: for 0 < c, a V-member annihilated by Q_T is zero. Immediate corollary of the energy concentration: Q_T v = 0 forces c ‖v‖² ≤ 0, and c > 0 gives v = 0.

The Gram lower bound G ≥ c·I on an orthonormal basis of V: for a ℂ-orthonormal family u inside V = prolateEigenspaceSup T W c and real coefficients b, the quadratic form of A on the combination x = ∑ᵢ bᵢ • uᵢ dominates c ∑ᵢ bᵢ²: c ∑ᵢ bᵢ² ≤ Re⟪A x, x⟫.

This is the operator matrix lower bound the pre-equalizer uses to get G⁻¹ ≤ (1/c)I. No per-vector eigenvalue μᵢ is used (u is only assumed orthonormal, not an eigenbasis): x ∈ V because V is a submodule, ‖x‖² = ∑ᵢ bᵢ² because u is orthonormal, and le_inner_timeBandLimitingOp_of_mem supplies c ‖x‖² ≤ Re⟪A x, x⟫ on V.

Pointwise ℝ → ℝ lift of an Lp class supported in the window. A star-fixed L²(ℝ;ℂ) element that is a.e.-supported in [0,T] — the shape Q_T ψ takes for a star-fixed ψ ∈ V — has a pointwise real representative supported in [0,T]: a function f : ℝ → ℝ with f in L², Function.support f ⊆ [0,T] pointwise, and (f : ℝ → ℂ) a.e. equal to the given class.

This is what the ContAwgnCode.testFn construction costs: it converts an a.e. equivalence class into the pointwise ℝ → ℝ function the structure field testFn demands, pinning both the pointwise support (testFn_support) and the real-valuedness. Once the a.e. identity (f : ℝ → ℂ) =ᵐ u is in hand, every integral/inner-product fact about the family (orthonormality, energy) transfers from the Lp inner product for free, so a single lift lemma sizes the whole conversion. The representative is 𝟙_[0,T] · Re(u); the indicator pins the support pointwise while staying in the same class because u already vanishes a.e. off [0,T], and Re recovers a real representative because u is star-fixed (a.e. real).

Pointwise ℝ → ℝ lift of an Lp class, without a support constraint. A star-fixed L²(ℝ;ℂ) element has a pointwise real representative: a function f : ℝ → ℝ in L² with (f : ℝ → ℂ) a.e. equal to the given class. This is the support-free sibling of exists_pointwise_repr_of_mem_timeLimit_star_fixed, needed for the band-limited encoder family whose members are not [0,T]-supported. The representative is Re ∘ u: it is L² because Re is a norm-1 Lipschitz image, and it recovers a representative of u because star-fixedness (star u = u) makes u a.e. real.

Band-limitedness transports from the frequency-support subspace to a pointwise real representative. If v ∈ bandLimitSubspace W and f : ℝ → ℝ complexifies to an a.e.-representative of v, then IsBandlimited f W. This is the bridge that lets the operator-theoretic bandLimitSubspace feed the L²-Fourier-support predicate IsBandlimited used by the ContAwgnCode band-limit constraint.

The real band-limited orthonormal encoder family for V = prolateEigenspaceSup T W c. Bundles the star-fixed ℂ-orthonormal basis u of V (needed to feed the operator lower bounds le_norm_timeLimitProj_sq_of_mem / le_re_inner_timeBandLimitingOp_sum_smul, which are stated on V) together with concrete real representatives h i : ℝ → ℝ of each u i, their L²-membership, the a.e. link (h i : ℂ) =ᵐ u i, band-limitedness IsBandlimited (h i) W, and the real orthonormality ∫ h i · h j = δ_{ij}. This is the encoder-side family the achievability receiver constructs signals from.