English
Define the 2-complement sequence Wᶜ₂: Z → R by Wᶜ₂(k) = (preNormEDS(b^4) c d (k−1)^2 · preNormEDS(b^4) c d (k+2) − preNormEDS(b^4) c d (k−2) · preNormEDS(b^4) c d (k+1)^2) × (If Even k then 1 else b).
Русский
Определяется 2-комплементная последовательность Wᶜ₂: ℤ → R как Wᶜ₂(k) = (preNormEDS(b^4) c d (k−1)^2 · preNormEDS(b^4) c d (k+2) − preNormEDS(b^4) c d (k−2) · preNormEDS(b^4) c d (k+1)^2) × (If Even k then 1 else b).
LaTeX
$$$$\text{complEDS}_2(b,c,d)(k) = \Big( \text{preNormEDS}(b^4) c d (k-1)^2 \cdot \text{preNormEDS}(b^4) c d (k+2) - \text{preNormEDS}(b^4) c d (k-2) \cdot \text{preNormEDS}(b^4) c d (k+1)^2 \Big) \cdot \begin{cases}1, & \text{Even } k \\ b, & \text{else} \end{cases}.$$$$
Lean4
/-- The 2-complement sequence `Wᶜ₂ : ℤ → R` for a normalised EDS `W : ℤ → R` that witnesses
`W(k) ∣ W(2 * k)`. In other words, `W(k) * Wᶜ₂(k) = W(2 * k)` for any `k ∈ ℤ`.
This is defined in terms of `preNormEDS`. -/
def complEDS₂ (k : ℤ) : R :=
(preNormEDS (b ^ 4) c d (k - 1) ^ 2 * preNormEDS (b ^ 4) c d (k + 2) -
preNormEDS (b ^ 4) c d (k - 2) * preNormEDS (b ^ 4) c d (k + 1) ^ 2) *
if Even k then 1 else b
