Euclid Numbers

This file introduces the Euclid numbers as defined in [GKP89]. This is sequence A129871 in [OEISFI25]

Implementation notes

The reference [GKP89] names the sequence $(e_n)_{n\ge 1}$ as Euclid numbers, while [OEISFI25] names it $(e_n)_{n\ge 0}$ as Sylvester's sequence. We chose to follow the notation from [GKP89].

Main results

• Recurrence with a product of Euclid numbers.
• Co-primality of Euclid numbers.
• Explicit formula.

References

• Concrete Mathematics
• The On-Line Encyclopedia of Integer Sequences

def Euclid.euclid : ℕ → ℕ

The sequence of Euclid numbers $(e_n)_{n\ge 0}$.

Definition by a simple recurrence. The more explicit recurrence is proved in Theorem euclid_prod_finset_add_one.

Equations

• Euclid.euclid 0 = 1
• Euclid.euclid 1 = 2
• Euclid.euclid n.succ = Euclid.euclid n ^ 2 - Euclid.euclid n + 1

@[simp]

theorem Euclid.euclid_zero : Euclid.euclid 0 = 1

@[simp]

theorem Euclid.euclid_one : Euclid.euclid 1 = 2

@[simp]

theorem Euclid.euclid_two : Euclid.euclid 2 = 3

@[simp]

theorem Euclid.euclid_three : Euclid.euclid 3 = 7

theorem Euclid.euclid_prod_finset_add_one {n : ℕ} : Euclid.euclid (n + 1) = ∏ x ∈ Finset.Icc 1 n, Euclid.euclid x + 1

The Euclid numbers satisfy the recurrence: $$ e_{n+1} = \prod_{i=1}^n e_i + 1. $$

theorem Euclid.euclid_prod_finset_add_one_of_pos {n : ℕ} (h : n ≥ 1) : Euclid.euclid n = ∏ x ∈ Finset.Icc 1 (n - 1), Euclid.euclid x + 1

Another expression of euclid_prod_finset_add_one for easier application when $n\ge 1$: $$ e_n = \prod_{i=1}^{n-1} e_i + 1. $$

theorem Euclid.euclid_gt_zero {n : ℕ} : 0 < Euclid.euclid n

Euclid numbers are positive.

theorem Euclid.euclid_ne_zero {n : ℕ} : NeZero (Euclid.euclid n)

theorem Euclid.euclid_ge_one {n : ℕ} : 1 ≤ Euclid.euclid n

Euclid numbers are $\ge 1$.

theorem Euclid.euclid_gt_one_of_pos {n : ℕ} (h : n ≥ 1) : 1 < Euclid.euclid n

Only $e_0 = 1$.

theorem Euclid.euclid_mod_eq_one {m n : ℕ} (h1 : m < n) (h2 : 0 < m) : Euclid.euclid n % Euclid.euclid m = 1

$e_n \equiv 1\ (\mathrm{mod}~e_m)$, when $0 < m < n$.

theorem Euclid.euclid_coprime {m n : ℕ} (h : m ≠ n) : (Euclid.euclid m).Coprime (Euclid.euclid n)

The Euclid numbers are co-prime: $\gcd(e_n, e_m) = 1$, for $n\neq m$.

theorem Euclid.euclid_strictMono : StrictMono Euclid.euclid

The Euclid numbers are strictly increasing: $e_n < e_{n+1}$, for all $n\in\mathbb{N}$.

noncomputable def Euclid.euclidConstant : ℝ

The sequence $$ \frac{1}{2^n}\log\left(e_n - \frac{1}{2}\right) $$ converges to $\log E$, where $E$ is the contant in the explicit formula for the Euclid numbers euclid_eq_floor_constant_pow.

Equations

• Euclid.euclidConstant = Real.exp Euclid.euclidLogConstant✝

theorem Euclid.euclidConstant_pos : 0 < Euclid.euclidConstant

$0 < E$.

theorem Euclid.euclid_le_constant_pow {n : ℕ} : ↑(Euclid.euclid n) ≤ Euclid.euclidConstant ^ 2 ^ n + 1 / 2

$e_n \le E^{2^n} + \frac{1}{2}$ for all $n\in\mathbb{N}$.

theorem Euclid.constant_pow_lt_euclid_add_one {n : ℕ} : Euclid.euclidConstant ^ 2 ^ n + 1 / 2 < ↑(Euclid.euclid n) + 1

$E^{2^n} + \frac{1}{2} < e_n + 1$ for all $n\in\mathbb{N}$.

theorem Euclid.euclid_eq_floor_constant_pow {n : ℕ} : Euclid.euclid n = ⌊Euclid.euclidConstant ^ 2 ^ n + 1 / 2⌋₊

$e_n = \lfloor E^{2^n} + \frac{1}{2}\rfloor$ for all $n\in\mathbb{N}$.