Type-I cosine transform for Chebyshev–Lobatto data

Let $n\in \mathbb{N}$ with $n\ge 1$ and let $y=(y_0,\dots ,y_n)\in {\mathbb{R}}^{n+1}$. In real-valued formulas, each natural index denotes its canonical real image (The canonical natural $\iota (n)=n\cdot 1_F$ of a field). Since $n>0$ by Canonical naturals are positive and strictly increasing, division by $n$ is defined in $\mathbb{R}$ (The reals form a field). The type-I discrete cosine transform, in the Lobatto convention used here, is the vector $X=(X_0,\dots ,X_n)$ defined by $X_k:=y_0+(-1{)}^k{y}_n+2{\sum }_{j=1}^{n-1}{y}_j\cos \text{\hspace{0.17em}⁣}\left(\frac{jk\pi }{n}\right),0\le k\le n\mathrm{.}$ Here $(-1{)}^k$ is the natural power of the real number $-1$ from Integer powers $a^m$, and the sum is the finite sum of Finite sums and finite products, by recursion, empty when $n=1$. The data $y_j$ are ordered from the right endpoint toward the left endpoint at nodes $\cos (j\pi \mathrm{/}n)$. This definition fixes the unnormalised DCT-I convention; the transform is not defined at $n=0$.