English
Define the integer-extended auxiliary sequence W: Z → R by W(n) = sgn(n) · preNormEDS′(b,c,d, |n|). This extends preNormEDS′ to negative indices by incorporating the sign of n.
Русский
Определяется целочисленно-расширенная вспомогательная последовательность W: ℤ → R так, что W(n) = sgn(n) · preNormEDS′(b,c,d, |n|). Это расширение preNormEDS′ на отрицательные индексы.
LaTeX
$$$$W(n) = \operatorname{sign}(n) \cdot \text{preNormEDS}'(b,c,d,|n|).$$$$
Lean4
/-- The auxiliary sequence for a normalised EDS `W : ℤ → R`, with initial values
`W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d` and extra parameter `b`.
This extends `preNormEDS'` by defining its values at negative integers. -/
def preNormEDS (n : ℤ) : R :=
n.sign * preNormEDS' b c d n.natAbs
