English
Same relation as above: preNormEDS(b^4) c d k · complEDS₂(b,c,d) k = preNormEDS(b^4) c d (2k) · (if Even k then 1 else b).
Русский
Та же зависимость: preNormEDS(b^4) c d k · complEDS₂(b,c,d) k = preNormEDS(b^4) c d (2k) · (если k чётное тогда 1, иначе b).
LaTeX
$$$$\text{preNormEDS}(b^4) c d k \cdot \text{complEDS}_2(b,c,d) k = \text{preNormEDS}(b^4) c d (2k) \cdot \big(\text{Even } k \?\, 1 \\: b\big).$$$$
Lean4
/-- The canonical example of a normalised EDS `W : ℤ → R`, with initial values
`W(0) = 0`, `W(1) = 1`, `W(2) = b`, `W(3) = c`, and `W(4) = d * b`.
This is defined in terms of `preNormEDS` whose even terms differ by a factor of `b`. -/
def normEDS (n : ℤ) : R :=
preNormEDS (b ^ 4) c d n * if Even n then b else 1
