Partial sum of a Fourier series

fourierCoeff f n

For an arbitrary function $f:\mathbb{R}\to\mathbb{C}$ and an arbitrary integer $n$, this quantity is defined as

i.e. one over $2\pi$ times the integral, taken from $-\pi$ to $\pi$ (in that orientation), of the product of $f(\theta)$ with $e^{-in\theta}$, where $n$ has been coerced to a complex number for the purposes of this exponent. The integral is Mathlib's total interval integral: if $f$ multiplied by $\theta\mapsto e^{-in\theta}$ is not interval-integrable on $[-\pi,\pi]$, the integral is assigned the junk value $0$, so $\text{fourierCoeff}(f,n)=0$ in that case. No hypothesis of continuity, integrability, or periodicity of $f$ is imposed or needed.

partialSum f N θ

For an arbitrary $f:\mathbb{R}\to\mathbb{C}$, an arbitrary natural number $N$, and an arbitrary real number $\theta$, this quantity is defined as the finite sum

where the summation index $n$ ranges over all integers $n$ satisfying $-N \le n \le N$, i.e. exactly $2N+1$ terms are summed for every $N$ ($N$ negative indices, the index $0$, and $N$ positive indices). In the special case $N=0$, the index set collapses to $\{0\}$, so $\text{partialSum}(f,0,\theta) = \text{fourierCoeff}(f,0)\cdot e^{i\cdot 0\cdot\theta} = \text{fourierCoeff}(f,0)$ — independent of $\theta$, and equal to $\tfrac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta')\,d\theta'$ (or $0$ under the same junk-value convention if that integral fails to exist). No continuity, integrability, or periodicity hypothesis on $f$ is assumed or required anywhere in this definition.