Elliptic divisibility sequences

This file defines the type of an elliptic divisibility sequence (EDS) and a few examples.

Mathematical background

Let $R$ be a commutative ring. An elliptic sequence is a sequence $W : \mathbb{Z} \to R$ satisfying $$ W(m + n)W(m - n)W(r)^2 = W(m + r)W(m - r)W(n)^2 - W(n + r)W(n - r)W(m)^2, $$ for any $m, n, r \in \mathbb{Z}$. A divisibility sequence is a sequence $W : \mathbb{Z} \to R$ satisfying $W(m) \mid W(n)$ for any $m, n \in \mathbb{Z}$ such that $m \mid n$.

Some examples of EDSs include

• the identity sequence,
• certain terms of Lucas sequences, and
• division polynomials of elliptic curves.

Main definitions

• IsEllSequence: a sequence indexed by integers is an elliptic sequence.
• IsDivSequence: a sequence indexed by integers is a divisibility sequence.
• IsEllDivSequence: a sequence indexed by integers is an EDS.
• normEDS': the canonical example of a normalised EDS indexed by ℕ.
• normEDS: the canonical example of a normalised EDS indexed by ℤ.

Main statements

• TODO: prove that normEDS satisfies IsEllDivSequence.
• TODO: prove that a normalised sequence satisfying IsEllDivSequence can be given by normEDS.

Implementation notes

IsEllDivSequence' b c d n is defined in terms of the private IsEllDivSequence'' b c d n, which are equal when n is odd and differ by a factor of b when n is even. This coincides with the reference since both agree for IsEllDivSequence' b c d 2 and for IsEllDivSequence' b c d 4, and the correct factors of b are removed in IsEllDivSequence' b c d (2 * (m + 2) + 1) and in IsEllDivSequence' b c d (2 * (m + 3)). This is done to avoid the necessity for ring division by b in the inductive definition of IsEllDivSequence' b c d (2 * (m + 3)). The idea is that, an easy lemma shows that IsEllDivSequence' b c d (2 * (m + 3)) always contains a factor of b, so it is possible to remove a factor of b a posteriori, but stating this lemma requires first defining IsEllDivSequence' b c d (2 * (m + 3)), which requires having this factor of b a priori.

References

M Ward, Memoir on Elliptic Divisibility Sequences

Tags

elliptic, divisibility, sequence

def IsEllSequence {R : Type u} [CommRing R] (W : ℤ → R) : Prop

The proposition that a sequence indexed by integers is an elliptic sequence.

Equations

• IsEllSequence W = ∀ (m n r : ℤ), W (m + n) * W (m - n) * W r ^ 2 = W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2

def IsDivSequence {R : Type u} [CommRing R] (W : ℤ → R) : Prop

The proposition that a sequence indexed by integers is a divisibility sequence.

Equations

• IsDivSequence W = ∀ (m n : ℕ), m ∣ n → W ↑m ∣ W ↑n

def IsEllDivSequence {R : Type u} [CommRing R] (W : ℤ → R) : Prop

The proposition that a sequence indexed by integers is an EDS.

Equations

• IsEllDivSequence W = (IsEllSequence W ∧ IsDivSequence W)

theorem IsEllSequence_id : IsEllSequence id

theorem IsDivSequence_id : IsDivSequence id

theorem IsEllDivSequence_id : IsEllDivSequence id

The identity sequence is an EDS.

theorem IsEllSequence_mul {R : Type u} [CommRing R] (x : R) {W : ℤ → R} (h : IsEllSequence W) : IsEllSequence (x • W)

theorem IsDivSequence_mul {R : Type u} [CommRing R] (x : R) {W : ℤ → R} (h : IsDivSequence W) : IsDivSequence (x • W)

theorem IsEllDivSequence_mul {R : Type u} [CommRing R] (x : R) {W : ℤ → R} (h : IsEllDivSequence W) : IsEllDivSequence (x • W)

def normEDS' {R : Type u} [CommRing R] (b : R) (c : R) (d : R) (n : ℕ) : R

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) = b * d.

This is defined in terms of a truncated sequence whose even terms differ by a factor of b.

Equations

• normEDS' b c d n = normEDS'' b c d n * if Even n then b else 1

@[simp]

theorem normEDS'_zero {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS' b c d 0 = 0

@[simp]

theorem normEDS'_one {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS' b c d 1 = 1

@[simp]

theorem normEDS'_two {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS' b c d 2 = b

@[simp]

theorem normEDS'_three {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS' b c d 3 = c

@[simp]

theorem normEDS'_four {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS' b c d 4 = d * b

theorem normEDS'_odd {R : Type u} [CommRing R] (b : R) (c : R) (d : R) (m : ℕ) : normEDS' b c d (2 * (m + 2) + 1) = normEDS' b c d (m + 4) * normEDS' b c d (m + 2) ^ 3 - normEDS' b c d (m + 1) * normEDS' b c d (m + 3) ^ 3

theorem normEDS'_even {R : Type u} [CommRing R] (b : R) (c : R) (d : R) (m : ℕ) : normEDS' b c d (2 * (m + 3)) * b = normEDS' b c d (m + 2) ^ 2 * normEDS' b c d (m + 3) * normEDS' b c d (m + 5) - normEDS' b c d (m + 1) * normEDS' b c d (m + 3) * normEDS' b c d (m + 4) ^ 2

def normEDS {R : Type u} [CommRing R] (b : R) (c : R) (d : R) (n : ℤ) : R

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) = b * d.

This extends normEDS' by defining its values at negative integers.

Equations

• normEDS b c d n = ↑(Int.sign n) * normEDS' b c d (Int.natAbs n)

@[simp]

theorem normEDS_zero {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS b c d 0 = 0

@[simp]

theorem normEDS_one {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS b c d 1 = 1

@[simp]

theorem normEDS_two {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS b c d 2 = b

@[simp]

theorem normEDS_three {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS b c d 3 = c

@[simp]

theorem normEDS_four {R : Type u} [CommRing R] (b : R) (c : R) (d : R) : normEDS b c d 4 = d * b

theorem normEDS_odd {R : Type u} [CommRing R] (b : R) (c : R) (d : R) (m : ℕ) : normEDS b c d (2 * (↑m + 2) + 1) = normEDS b c d (↑m + 4) * normEDS b c d (↑m + 2) ^ 3 - normEDS b c d (↑m + 1) * normEDS b c d (↑m + 3) ^ 3

theorem normEDS_even {R : Type u} [CommRing R] (b : R) (c : R) (d : R) (m : ℕ) : normEDS b c d (2 * (↑m + 3)) * b = normEDS b c d (↑m + 2) ^ 2 * normEDS b c d (↑m + 3) * normEDS b c d (↑m + 5) - normEDS b c d (↑m + 1) * normEDS b c d (↑m + 3) * normEDS b c d (↑m + 4) ^ 2

@[simp]

theorem normEDS_neg {R : Type u} [CommRing R] (b : R) (c : R) (d : R) (n : ℕ) : normEDS b c d (-↑n) = -normEDS b c d ↑n