Fourier coefficient

For an arbitrary function $f : \mathbb{R} \to \mathbb{C}$ (no continuity, periodicity, or integrability assumption is imposed anywhere in this definition) and an arbitrary integer $n \in \mathbb{Z}$ (which may be positive, negative, or zero), the definition sets

where every piece is to be read literally as follows: $\pi$ is the real constant $\mathrm{Real.pi}$; the scalar factor $1/(2\pi)$ is the real number $1/(2\pi)$ regarded as a complex number (zero imaginary part), multiplying everything that follows; the integer $n$ is cast to a complex number and the real integration variable $\theta$ is likewise cast to a complex number solely for forming the exponent, so the exponent is exactly the complex number $-(n)\cdot\theta\cdot i$, i.e. $\exp(-in\theta) = \cos(n\theta) - i\sin(n\theta)$ by Euler's formula, a point on the unit circle in $\mathbb{C}$; and $\int_{-\pi}^{\pi}(\cdot)\,d\theta$ denotes Mathlib's interval integral with lower limit $-\pi$ and upper limit $\pi$, which — since $-\pi<\pi$ always — is here simply the ordinary (positively oriented, no sign reversal) integral of the complex-valued integrand $\theta \mapsto f(\theta)\exp(-in\theta)$ over $[-\pi,\pi]$; $f(\theta)$ and $\exp(-in\theta)$ are multiplied together as complex numbers before integrating. Because Mathlib's interval integral is a total (junk-valued) operator and $f$ carries no integrability hypothesis, if $\theta \mapsto f(\theta)\exp(-in\theta)$ is not interval-integrable on $[-\pi,\pi]$ the integral is simply assigned the junk value $0 \in \mathbb{C}$, and consequently $\mathrm{fourierCoeff}(f,n) = \tfrac{1}{2\pi}\cdot 0 = 0$ in that case, with no error, exception, or further condition raised — this includes, in particular, any $f$ for which $f(\theta)\exp(-in\theta)$ is unbounded, discontinuous in a bad way, or otherwise fails Bochner-integrability on that interval. In the case $n=0$, the exponential factor collapses identically to $\exp(0)=1$, so the formula reduces to $\mathrm{fourierCoeff}(f,0) = \tfrac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta)\,d\theta$ (again equal to $0$ if that plain integral of $f$ fails to exist in the integrability sense). For a negative index, writing $n=-m$ with $m$ a positive integer, the coerced quantity $-(n:\mathbb C)$ equals $+m$, so the exponent becomes $+im\theta$ rather than $-im\theta$ — i.e. passing from a positive index to its negation exactly reverses the sign in the exponent, with no complex-conjugation, absolute value, or other transformation of $f$ or of the integral applied anywhere; the same single closed formula above is evaluated verbatim for every integer $n$ (positive, negative, or zero) and every function $f$, with the stated real-to-complex casts of $n$, $\theta$, and $\pi$, and the junk-value convention on non-integrable integrands, being the only implicit steps.