Sylvester’s sequence

Content created by Egbert Rijke, Fredrik Bakke and Louis Wasserman.

Created on 2024-10-25.
Last modified on 2025-08-30.

module elementary-number-theory.sylvesters-sequence where
Imports 
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.ordinal-induction-natural-numbers
open import elementary-number-theory.products-of-natural-numbers

open import univalent-combinatorics.standard-finite-types

Idea

Sylvester’s sequence is the sequence s of natural numbers in which s n is the successor of the product of all the numbers s i for i < n, i.e.,

The first few entries in this sequence are s 0 = 2, s 1 = 3, s 2 = 7, and s 3 = 43.

Sylvester’s sequence is listed as A000058 in the OEIS [OEIS].

Definitions

sylvesters-sequence-ℕ : ℕ → ℕ
sylvesters-sequence-ℕ =
  ordinal-ind-ℕ
    ( λ _ → ℕ)
    ( λ n f →
      succ-ℕ (Π-ℕ n (λ i → f (nat-Fin n i) (strict-upper-bound-nat-Fin n i))))

References

[OEIS]
OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences. website. URL: https://oeis.org.

Recent changes