Documentation

SpecialNumbers.Sylvester

Sylvester sequence #

This file introduces the Sylvester's sequence. This is sequence A000058 in [OEISFI25].

Implementation notes #

We follow the presentantion from Wikipedia.

Main results #

References #

source
def sylvester :
ℕ → ℕ

Sylvester sequence: https://oeis.org/A000058.

Equations
Instances For
    source
    @[simp]
    theorem sylvester_zero :
    sylvester 0 = 2
    source
    @[simp]
    theorem sylvester_one :
    sylvester 1 = 3
    source
    @[simp]
    theorem sylvester_two :
    sylvester 2 = 7
    source
    @[simp]
    theorem sylvester_three :
    sylvester 3 = 43
    source
    theorem sylvester_ge_two (n : ℕ) :
    2 ≤ sylvester n
    source
    theorem sylvester_prod_finset_add_one {n : ℕ} :
    sylvester n = ∏ i ∈ Finset.range n, sylvester i + 1

    This recurrence motivates the alternative name of Euclid numbers: $$ \mathrm{sylvester}~n = 1 + \prod_{i=0}^{n-1} \mathrm{sylvester}~i, $$ assuming the product over the empty set to be 1.

    source
    theorem sylvester_strictMono :
    StrictMono sylvester
    source
    theorem sylvester_mod_eq_one {m n : ℕ} (h1 : m < n) :
    sylvester n % sylvester m = 1
    source
    theorem sylvester_coprime {m n : ℕ} (h : m ≠ n) :
    (sylvester m).Coprime (sylvester n)
    source
    noncomputable def sylvesterConstant :
    ℝ

    The constant that gives an explicit formula for the Sylvester sequence: $$ \mathrm{sylvester}~n = \left\lfloor\mathrm{sylvesterConstant}^{2^{n+1}} + \frac{1}{2}\right\rfloor, $$ for all natural $n$. The constant is approximately $1.2640847\ldots$.

    Equations
    Instances For
      source
      theorem sylvesterConstant_pos :
      0 < sylvesterConstant
      source
      theorem sylvester_eq_floor_constant_pow {n : ℕ} :
      sylvester n = ⌊sylvesterConstant ^ 2 ^ (n + 1) + 1 / 2⌋₊

      Explicit formula for the Sylvester sequence: $$ \mathrm{sylvester}~n = \left\lfloor\mathrm{sylvesterConstant}^{2^{n+1}} + \frac{1}{2}\right\rfloor, $$ for all natural $n$.