Stern's diatomic sequence

DefinitionStern's diatomic sequence#✓fully proved

The Stern sequence is the function \(s : \mathbb{N} \to \mathbb{N}\) defined by \(s(0) = 0\), \(s(1) = 1\), and, for every \(n \ge 1\), \(s(2n) = s(n)\) and \(s(2n + 1) = s(n) + s(n + 1)\).

def sternSequence : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 =>
    if h : (n + 2) % 2 = 0 then sternSequence ((n + 2) / 2)
    else sternSequence ((n + 2) / 2) + sternSequence ((n + 2) / 2 + 1)
termination_by n => n
decreasing_by all_goals omega

Sources

• Stern sequence ("Stern diatomic sequence", OEIS A002487); JIS Lansing, lines 92-103; JIS Dennison, lines 80-85.

Used by 4

Used byEven-index recurrence for the Stern sequence · Odd-index recurrence for the Stern sequence · Stern sequence at one · Stern sequence at zero

TheoremStern sequence at zero#✓fully proved

The Stern sequence \(s\) satisfies \(s(0) = 0\).

theorem stern_zero : sternSequence 0 = 0

Sources

• Stern sequence, OEIS A002487; JIS Lansing, lines 92-103.

Uses 1

Statement usesStern's diatomic sequence

TheoremStern sequence at one#✓fully proved

The Stern sequence \(s\) satisfies \(s(1) = 1\).

theorem stern_one : sternSequence 1 = 1

Sources

• Stern sequence, OEIS A002487; JIS Lansing, lines 92-103.

Uses 1

Statement usesStern's diatomic sequence

TheoremEven-index recurrence for the Stern sequence#✓fully proved

For every natural number \(n \ge 1\), the Stern sequence \(s\) satisfies \(s(2n) = s(n)\).

theorem stern_even (n : Nat) (hn : 1 ≤ n) : sternSequence (2 * n) = sternSequence n

Sources

• Stern sequence, OEIS A002487; JIS Lansing, lines 92-103; JIS Dennison, lines 80-85.

Uses 1

Statement usesStern's diatomic sequence

TheoremOdd-index recurrence for the Stern sequence#✓fully proved

For every natural number \(n \ge 1\), the Stern sequence \(s\) satisfies \(s(2n + 1) = s(n) + s(n + 1)\).

theorem stern_odd (n : Nat) (hn : 1 ≤ n) :
    sternSequence (2 * n + 1) = sternSequence n + sternSequence (n + 1)

Sources

• Stern sequence, OEIS A002487; JIS Lansing, lines 92-103; JIS Dennison, lines 80-85.

Uses 1

Statement usesStern's diatomic sequence

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.