Fungrim entry: 2a8ec9

\left(\begin{cases} \sum_{k=0}^{N} {a}_{k} < 2 \pi, & N = 0\\\sum_{k=0}^{N} {a}_{k} \le 2 \pi, & N \ge 1\\ \end{cases}\right) \;\implies\; \left(\sum_{n=-\infty}^{\infty} \prod_{k=0}^{N} \operatorname{sinc}\!\left({a}_{k} n\right) = \int_{-\infty}^{\infty} \prod_{k=0}^{N} \operatorname{sinc}\!\left({a}_{k} x\right) \, dx\right)

Assumptions:

N \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; {a}_{k} \in \left(0, \infty\right)

References:

https://www.carma.newcastle.edu.au/resources/jon/sinc-sums.pdf

TeX:

\left(\begin{cases} \sum_{k=0}^{N} {a}_{k} < 2 \pi, & N = 0\\\sum_{k=0}^{N} {a}_{k} \le 2 \pi, & N \ge 1\\ \end{cases}\right) \;\implies\; \left(\sum_{n=-\infty}^{\infty} \prod_{k=0}^{N} \operatorname{sinc}\!\left({a}_{k} n\right) = \int_{-\infty}^{\infty} \prod_{k=0}^{N} \operatorname{sinc}\!\left({a}_{k} x\right) \, dx\right)

N \in \mathbb{Z}_{\ge 0} \;\mathbin{\operatorname{and}}\; {a}_{k} \in \left(0, \infty\right)

Definitions:

Fungrim symbol	Notation	Short description
`Sum`	$\sum_{n} f(n)$	Sum
`Pi`	$\pi$	The constant pi (3.14...)
`Product`	$\prod_{n} f(n)$	Product
`Sinc`	$\operatorname{sinc}(z)$	Sinc function
`Infinity`	$\infty$	Positive infinity
`Integral`	$\int_{a}^{b} f(x) \, dx$	Integral
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n
`OpenInterval`	$\left(a, b\right)$	Open interval

Source code for this entry:

Entry(ID("2a8ec9"),
    Formula(Implies(Cases(Tuple(Less(Sum(Subscript(a, k), For(k, 0, N)), Mul(2, Pi)), Equal(N, 0)), Tuple(LessEqual(Sum(Subscript(a, k), For(k, 0, N)), Mul(2, Pi)), GreaterEqual(N, 1))), Equal(Sum(Product(Sinc(Mul(Subscript(a, k), n)), For(k, 0, N)), For(n, Neg(Infinity), Infinity)), Integral(Product(Sinc(Mul(Subscript(a, k), x)), For(k, 0, N)), For(x, Neg(Infinity), Infinity))))),
    Variables(N, a),
    Assumptions(And(Element(N, ZZGreaterEqual(0)), Element(Subscript(a, k), OpenInterval(0, Infinity)))),
    References("https://www.carma.newcastle.edu.au/resources/jon/sinc-sums.pdf"))

Topics using this entry

Sinc function