Documentation

LeanPool.SpecialNumbers.Euclidian

Euclid Numbers #

This file introduces the Euclid numbers as defined in [knuth1989concrete]. This is sequence A129871 in [oeis]

Implementation notes #

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

Main results #

References #

source
def SpecialNumbers.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
Instances For
    source
    @[simp]
    theorem SpecialNumbers.Euclid.euclid_zero :
    euclid 0 = 1
    source
    @[simp]
    theorem SpecialNumbers.Euclid.euclid_one :
    euclid 1 = 2
    source
    @[simp]
    theorem SpecialNumbers.Euclid.euclid_two :
    euclid 2 = 3
    source
    @[simp]
    theorem SpecialNumbers.Euclid.euclid_three :
    euclid 3 = 7
    source
    theorem SpecialNumbers.Euclid.euclid_prod_finset_add_one {n : ℕ} :
    euclid (n + 1) = ∏ x ∈ Finset.Icc 1 n, euclid x + 1

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

    source
    theorem SpecialNumbers.Euclid.euclid_prod_finset_add_one_of_pos {n : ℕ} (h : n ≥ 1) :
    euclid n = ∏ x ∈ Finset.Icc 1 (n - 1), 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. $$

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

    Euclid numbers are positive.

    source
    theorem SpecialNumbers.Euclid.euclid_ne_zero {n : ℕ} :
    NeZero (euclid n)
    source
    theorem SpecialNumbers.Euclid.euclid_ge_one {n : ℕ} :
    1 ≤ euclid n

    Euclid numbers are $\ge 1$.

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

    Only $e_0 = 1$.

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

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

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

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

    source
    theorem SpecialNumbers.Euclid.euclid_strictMono :
    StrictMono euclid

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

    source
    noncomputable def SpecialNumbers.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
    Instances For
      source
      theorem SpecialNumbers.Euclid.euclidConstant_pos :
      0 < euclidConstant

      $0 < E$.

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

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

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

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

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

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