English
complEDS' is a complement sequence defined for a normalised elliptic divisibility sequence, with a base case and a division-like recurrence depending on parity of n.
Русский
complEDS' — это дополнение к последовательности для нормализованной эллиптической последовательности делимости, имеющее базовый случай и рекуррентное отношение, зависящее от парности n.
LaTeX
$$$\text{complEDS}' : \mathbb{N} \to R \quad (0\mapsto 0), (1\mapsto 1),\ (n+2)\mapsto \begin{cases} \text{complEDS}'(m) \cdot \text{complEDS}_2(b,c,d)(m\cdot k) & \text{if } n \text{ is even}, \\ \text{complicated expression} & \text{otherwise} \end{cases}$$$
Lean4
/-- The complement sequence `Wᶜ : ℤ × ℕ → R` for a normalised EDS `W : ℤ → R` that witnesses
`W(k) ∣ W(n * k)`. In other words, `W(k) * Wᶜ(k, n) = W(n * k)` for any `k, n ∈ ℤ`.
This is defined in terms of `normEDS` and agrees with `complEDS₂` when `n = 2`. -/
def complEDS' : ℕ → R
| 0 => 0
| 1 => 1
| (n + 2) =>
let m := n / 2 + 1
if hn : Even n then complEDS' m * complEDS₂ b c d (m * k)
else
have : m + 1 < n + 2 := add_lt_add_right (Nat.div_lt_self (Nat.not_even_iff_odd.mp hn).pos one_lt_two) 2
complEDS' m ^ 2 * normEDS b c d ((m + 1) * k + 1) * normEDS b c d ((m + 1) * k - 1) -
complEDS' (m + 1) ^ 2 * normEDS b c d (m * k + 1) * normEDS b c d (m * k - 1)
