A real signal f : ℝ → ℝ is band-limited to [-W, W] if the L²-Fourier transform of its complexification has spectral support in [-W, W], i.e. vanishes almost everywhere on {ξ | W < |ξ|}. The complexification t ↦ (f t : ℂ) is needed because the L² Fourier transform 𝓕 : Lp ℂ 2 volume → Lp ℂ 2 volume is complex-valued.

This is a band-limit constraint: unlike the L¹ Real.fourierIntegral (which is 0 for every non-L¹ signal, hence vacuous — junk-0 — on the entire target class of essentially time-limited band-limited L² signals), the L² transform is defined on the whole a.e. class and its support separates band-limited functions from broadband ones.

The L²-L¹ Fourier-agreement bridge: for f ∈ L¹ ∩ L², the coeFn of the L²-Fourier transform of the canonical Lp representative of f agrees almost everywhere with the classical L¹ Fourier integral 𝓕 f (the pointwise VectorFourier.fourierIntegral).

This is the plumbing that connects the abstract L²-Fourier isometry 𝓕 : Lp ℂ 2 → Lp ℂ 2 to the concrete pointwise integral, over the tempered-distribution scaffolding. Both objects define the same tempered distribution: the L²-Fourier side via Lp.fourier_toTemperedDistribution_eq, the L¹ pointwise side via the Fourier self-adjointness (multiplication formula) VectorFourier.integral_fourierIntegral_smul_eq_flip; equality of tempered distributions on the locally integrable class forces almost-everywhere equality (ae_eq_of_integral_contDiff_smul_eq).

@audit:ok

The L²-L¹ inverse-Fourier-agreement bridge, the inverse-transform sibling of l2Fourier_eq_fourierIntegral: for f ∈ L¹ ∩ L², the coeFn of the L²-inverse-Fourier transform of the canonical Lp representative agrees almost everywhere with the classical L¹ inverse Fourier integral 𝓕⁻ f. Used by bandlimited_sup_bound to realize a band-limited signal as the inverse transform of its (compactly supported, hence L¹) spectrum.

@audit:ok

Paley-Wiener sup bound: a continuous band-limited L² signal is bounded pointwise by its L² energy, |f t| ≤ √(2W)·‖f‖₂. Continuity pins the raw codeword to the canonical representative, and this bound caps the sample values by the codeword energy — dissolving the pointwise-vs-a.e. defect that made an encoder-only code unbounded.

The proof realizes the signal as the inverse Fourier transform of its (compactly supported, hence L¹) spectrum via l2FourierInv_eq_fourierIntegralInv, bounds the pointwise inverse transform by the L¹ norm of the spectrum, and closes with Hölder on [-W, W] and Plancherel.

@audit:ok

A continuous-time AWGN code over the window [0, T] with bandwidth W, average power P, and M messages.

The encoder maps each message to a band-limited function ℝ → ℝ (never a fixed sample vector — this is what keeps the definition non-circular), whose whole-line energy is at most T · P. The receiver does not read the codeword pointwise; it correlates it against k orthonormal test functions supported in [0, T], observing the vector i ↦ ∫ (encoder m)·(testFn i) corrupted by independent Gaussian noise (ContAwgnCode.observation, ContAwgnCode.errorProbAt). This is the textbook Karhunen-Loève / matched-filter discretization of the channel: against an orthonormal family the coefficients of white noise are exactly i.i.d. N(0, N₀/2), which is what makes the product law Measure.pi in errorProbAt an exact description of the physical channel rather than a surrogate for one. A point-sampling observation map would be an isometry only at the Nyquist spacing — i.e. calibrated at exactly the value the Shannon-Hartley identity has to prove; see docs/shannon/shannon-hartley-facts.md §OBSERVATION-MAP for the non-circularity argument.

The observation count k is a free ℕ field, and no field mentions 2W or ⌊2WT⌋: testFn is asked only to be orthonormal and supported in [0, T], and the W in encoder_bandlimited is a physical bandwidth, not a dimension count. The ≈ 2WT degrees-of-freedom count is therefore not available from this definition. It has to come from the prolate-spheroidal eigenvalue distribution: a band-limited f satisfies ∫ f·φᵢ = ⟪f, P_W φᵢ⟫, so the Gram matrix of the test family is a compression of the time-band-limiting operator of TimeBandLimiting.lean, and how many of its eigenvalues sit near 1 is exactly the Landau-Pollak-Slepian count.

The noiseless observation of message m along the i-th test function: the correlation ∫ (encoder m)·(testFn i) of the codeword with the matched filter testFn i.

This is the analysis half of the Karhunen-Loève discretization. It depends on encoder m only through its a.e. class, and is finite because encoder_memLp and testFn_memLp put both factors in L². Since testFn i is supported in [0, T], the integral only sees the codeword during the transmission window; since encoder m is band-limited, ∫ f·φᵢ = ⟪f, P_W φᵢ⟫, which is what routes the degrees-of-freedom question to the spectrum of the time-band-limiting operator.

Point-wise error probability for message m: the noisy observation vector y = ContAwgnCode.observation m + noise (per-observation noise variance N₀/2, independent across observations) lands in the decoding-error region {y | decoder y ≠ m}.

Modeled directly as Measure.pi (fun i => gaussianReal (observationᵢ) (N₀/2)), i.e. the memoryless per-observation AWGN law — the same law computed by the discrete ChannelCoding.Code.errorProbAt for awgnChannel (N₀/2), but inlined so that no IsAwgnChannelMeasurable kernel-measurability hypothesis is needed inside the definition.

The product law is exact here, not an approximation: the noise coefficients are ⟪ξ, φᵢ⟫ for the orthonormal family testFn, and the coefficients of white noise along an orthonormal family are i.i.d. N(0, N₀/2) for that family alone — no spacing, rate or bandwidth condition enters. This is what ContAwgnCode.testFn_orthonormal buys.

Average error probability under a uniform message: (1/M) ∑ₘ errorProbAt m (0 for the empty code M = 0).

The largest number of messages distinguishable over the window [0, T] with average error probability at most ε — an operational primitive that contains no 2W or ⌊2WT⌋.

The per-second rate achievable at error level ε: limsup_T (log M(T, ε)) / T.

The operational capacity of the continuous-time band-limited AWGN channel: the per-second rate in the vanishing-error limit, ⨅_{ε ∈ (0,1)} contAwgnRate W N₀ P ε. The infimum over ε extracts the ε → 0 capacity; ε is restricted to (0, 1) because ε ≥ 1 is satisfied by every code (average error is ≤ 1) and would make the message set unbounded.

The infimum is taken over the subtype ↥(Set.Ioo 0 1), not via the bounded-binder ⨅ ε ∈ Set.Ioo 0 1. The two are not the same for the conditionally-complete order ℝ: the bounded-binder form unfolds to ⨅ ε, ⨅ (_ : ε ∈ Set.Ioo 0 1), contAwgnRate …, and for every ε ∉ (0, 1) the inner ⨅ ranges over an empty index, contributing the junk value sInf ∅ = 0. Since contAwgnRate ≥ 0, that phantom 0 collapses the whole infimum to 0, making both contAwgn_ge_shannonHartley and contAwgn_eq_shannonHartley false as framed for P > 0. The subtype infimum ranges only over (0, 1) and carries no phantom.