Recurrences and generating functions

Lens

MotivationH

Counting by remembering

A drummer in a Carnatic ensemble, or a poet composing in Sanskrit or Prakrit, builds rhythms from short beats (one unit of time) and long beats (two units). How many different rhythms fill exactly $n$ units? For $n = 1, 2, 3, 4, 5$ there are $1, 2, 3, 5, 8$ . Indian prosodists noticed — more than five centuries before Leonardo of Pisa wrote about rabbits — that each count is the sum of the previous two: a rhythm of length $n$ either ends with a short beat (after a rhythm of length $n - 1$ ) or with a long beat (after a rhythm of length $n - 2$ ).

That one observation is a recurrence: it defines a sequence by its own past. Recurrences are everywhere. The number of moves needed to solve the Tower of Hanoi, the running time of mergesort, the balance of a loan in Nairobi or Lima with monthly interest and repayments, the population of a species with age classes, the number of ways to bracket a long product — each is described most naturally by saying how the next value depends on the earlier ones.

This lesson answers three questions about such sequences:

Exact solution. When can we replace "the next term is …" by a formula for the $n$ -th term? For linear recurrences with constant coefficients the answer is always, and the method is the characteristic polynomial.
Packaging. A generating function $\sum a_n x^n$ turns a whole sequence into a single algebraic object, so that recurrences become equations and counting problems become multiplication.
Growth. When an exact formula is out of reach — or too detailed to be useful — how fast does the sequence grow? This is the language of $O$ , $\Omega$ and $\Theta$ that every analysis of an algorithm uses.

You will need combinatorics (binomial coefficients, counting in two ways) and sequences and series (summation, induction, geometric series).

IntuitionH

Unroll, guess, verify — and the sequence as one object

Take the rhythms again, and write $t_n$ for the number of rhythms of length $n$ . We have $t_1 = 1$ , $t_2 = 2$ and $t_n = t_{n-1} + t_{n-2}$ . These are the Fibonacci numbers shifted by one: with $F_0 = 0$ , $F_1 = 1$ , $F_{n+2} = F_{n+1} + F_n$ we have $t_n = F_{n+1}$ . The same count answers "how many ways can a $1 \times n$ strip be tiled by squares and dominoes?":

The five tilings of a $1 \times 4$ strip by squares (short beats) and dominoes (long beats). Sorting them by the last tile — square or domino — shows $t_4 = t_3 + t_2 = 3 + 2$.

How would we ever find a formula for $F_n$ ? Two complementary ideas run through the lesson.

Guess an exponential. The numbers $1, 1, 2, 3, 5, 8, 13, 21, \dots$ grow by a factor that settles near $1.618$ . So try $a_n = r^n$ . Substituting into $a_{n+2} = a_{n+1} + a_n$ and dividing by $r^n$ gives $r^2 = r + 1$ — a quadratic equation, with two roots $\varphi = (1 + \sqrt5)/2$ and $\psi = (1 - \sqrt5)/2$ . The recurrence is linear, so any combination $A\varphi^n + B\psi^n$ is a solution too, and two free constants are exactly enough to match the two starting values.

Package the sequence. Write all the terms into one expression $F(x) = F_0 + F_1 x + F_2 x^2 + \cdots$ . The recurrence says that $F(x) - xF(x) - x^2F(x)$ has almost every coefficient zero, so $F(x) = x/(1 - x - x^2)$ : the infinite sequence is captured by a fraction of two tiny polynomials. Algebra on that fraction — partial fractions — gives back the same formula.

DefinitionsH

Definitions

Definition— recurrence relation

A recurrence relation for a sequence $(a_n)_{n \ge 0}$ expresses $a_n$ in terms of earlier terms. It is linear of order $k$ with constant coefficients if there are constants $c_1, \dots, c_k$ (real or complex) with $c_k \ne 0$ such that

a_{n+k} = c_1 a_{n+k-1} + c_2 a_{n+k-2} + \cdots + c_k a_n \qquad \text{for all } n \ge 0,

and homogeneous because there is no extra term depending only on $n$ . Adding a term $g(n)$ on the right gives an inhomogeneous recurrence. The values $a_0, \dots, a_{k-1}$ are the initial values.

Definition— characteristic polynomial

The characteristic polynomial of $a_{n+k} = c_1 a_{n+k-1} + \cdots + c_k a_n$ is

\chi(x) = x^k - c_1 x^{k-1} - c_2 x^{k-2} - \cdots - c_k .

Its roots (in $\C$ ) are the characteristic roots. For the Fibonacci recurrence, $\chi(x) = x^2 - x - 1$ .

Definition— ordinary generating function

The ordinary generating function of a sequence $(a_n)_{n \ge 0}$ is the formal power series

A(x) = \sum_{n \ge 0} a_n x^n = a_0 + a_1 x + a_2 x^2 + \cdots .

We write $[x^n]A(x) = a_n$ for "the coefficient of $x^n$ in $A$ ".

Definition— formal power series

For a field $K$ (we use $\Q$ , $\R$ or $\C$ ), the ring $K[[x]]$ of formal power series consists of all sequences $(a_n)_{n \ge 0}$ of elements of $K$ , written $\sum a_n x^n$ , with

\sum a_n x^n + \sum b_n x^n = \sum (a_n + b_n) x^n, \qquad \Big(\sum a_n x^n\Big)\Big(\sum b_n x^n\Big) = \sum_n \Big(\sum_{i=0}^{n} a_i b_{n-i}\Big) x^n .

Each coefficient of a sum or product is a finite computation, so no question of convergence ever arises: $x$ is a symbol, not a number. Polynomials are the series with finitely many non-zero coefficients.

Definition— asymptotic notation

Let $f, g$ be real-valued functions on $\N$ (or on $[1, \infty)$ ).

$f(n) = O(g(n))$ if there are constants $C > 0$ and $N$ with $|f(n)| \le C\,|g(n)|$ for all $n \ge N$ — " $f$ grows at most as fast as $g$ , up to a constant".
$f(n) = \Omega(g(n))$ if $g(n) = O(f(n))$ — at least as fast, up to a constant (Knuth's convention).
$f(n) = \Theta(g(n))$ if both $f = O(g)$ and $f = \Omega(g)$ .
$f(n) = o(g(n))$ if $f(n)/g(n) \to 0$ ; and $f(n) \sim g(n)$ if $f(n)/g(n) \to 1$ (for $g$ eventually non-zero).

The " $=$ " in $f = O(g)$ is a one-way abbreviation for " $f$ belongs to the class $O(g)$ ": $n = O(n^2)$ is true, but " $O(n^2) = n$ " means nothing.

Worked examplesH

Worked examples and non-examples

Example— Distinct real roots

Solve $a_{n+2} = 5a_{n+1} - 6a_n$ with $a_0 = 0$ , $a_1 = 1$ . The characteristic polynomial is $x^2 - 5x + 6 = (x - 2)(x - 3)$ , so $a_n = A\,2^n + B\,3^n$ . The initial values give $A + B = 0$ and $2A + 3B = 1$ , so $B = 1$ , $A = -1$ and

a_n = 3^n - 2^n: \qquad 0,\ 1,\ 5,\ 19,\ 65,\ 211,\ \dots

Check: $5 \cdot 19 - 6 \cdot 5 = 65$ . ✓

Example— A repeated root

Solve $a_{n+2} = 4a_{n+1} - 4a_n$ with $a_0 = 1$ , $a_1 = 4$ . Now $\chi(x) = x^2 - 4x + 4 = (x - 2)^2$ has the single root $2$ , and $A\,2^n + B\,2^n$ has only one free constant — not enough. The extra solution is $n\,2^n$ (proved below), so $a_n = (A + Bn)2^n$ . From $a_0 = A = 1$ and $a_1 = 2(A + B) = 4$ we get $B = 1$ : $a_n = (n + 1)2^n$ , giving $1, 4, 12, 32, 80, \dots$

Example— Complex roots give oscillation

The recurrence $a_{n+2} = -a_n$ has $\chi(x) = x^2 + 1$ with roots $\pm i$ . The general solution $A\,i^n + B(-i)^n$ can be rewritten with real constants as $C\cos(n\pi/2) + D\sin(n\pi/2)$ , since $i^n = \cos(n\pi/2) + i\sin(n\pi/2)$ . With $a_0 = 1$ , $a_1 = 0$ the solution is $1, 0, -1, 0, 1, 0, \dots$ : complex characteristic roots of modulus $1$ produce oscillation (here periodic), just as $y'' = -y$ produces $\cos t$ .

Example— The Tower of Hanoi: an inhomogeneous recurrence

To move $n$ discs, move the top $n - 1$ to the spare peg, move the largest disc, then move the $n - 1$ back on top: $H_n = 2H_{n-1} + 1$ , $H_0 = 0$ . Adding $1$ to both sides gives $H_n + 1 = 2(H_{n-1} + 1)$ , so $H_n + 1 = 2^n$ and $H_n = 2^n - 1$ . (One can also show that no solution uses fewer moves: the largest disc must move at least once, and before its first move all other discs sit on one peg.)

Example— Non-examples

$x_{n+1} = r x_n (1 - x_n)$ , the logistic map, is a recurrence but not linear; for $r = 4$ it is chaotic, and there is no characteristic polynomial to help.
$a_n = n\,a_{n-1}$ (so $a_n = n!\,a_0$ ) is linear but its coefficient depends on $n$ ; the characteristic method does not apply.
$a_{n+1} = a_n + a_{\lfloor n/2 \rfloor}$ refers back a variable distance; divide-and-conquer recurrences like this need other tools (see the section on growth).

ProofH

Linear recurrences: the characteristic-root theorem

We work with order $2$ , $a_{n+2} = p\,a_{n+1} + q\,a_n$ , where every idea is visible; the general statement follows the proofs.

Theorem— Lemma 1 (linearity)

If $(a_n)$ and $(b_n)$ satisfy $a_{n+2} = p\,a_{n+1} + q\,a_n$ , then so does $(A a_n + B b_n)$ for any constants $A, B$ . So the solutions form a vector space.

Proof

$A a_{n+2} + B b_{n+2} = A(p a_{n+1} + q a_n) + B(p b_{n+1} + q b_n) = p(A a_{n+1} + B b_{n+1}) + q(A a_n + B b_n)$ .

∎

Theorem— Lemma 2 (initial values determine the solution)

If two solutions $(a_n)$ and $(b_n)$ of the same recurrence satisfy $a_0 = b_0$ and $a_1 = b_1$ , then $a_n = b_n$ for all $n$ .

Proof

We prove by induction on $n$ the statement $P(n)$ : " $a_n = b_n$ and $a_{n+1} = b_{n+1}$ ". $P(0)$ is the hypothesis. If $P(n)$ holds, then $a_{n+1} = b_{n+1}$ , and

a_{n+2} = p\,a_{n+1} + q\,a_n = p\,b_{n+1} + q\,b_n = b_{n+2},

so $P(n+1)$ holds. Hence $a_n = b_n$ for all $n$ . (The induction must carry two consecutive terms because the recurrence looks back two steps.)

∎

Together, the lemmas say: the map sending a solution to its initial values $(a_0, a_1)$ is a linear bijection onto $K^2$ . The solution space has dimension exactly $2$ — and for a recurrence of order $k$ , dimension $k$ , by the same argument.

Theorem— Lemma 3 (geometric solutions)

$a_n = r^n$ is a solution if and only if $r^2 = p\,r + q$ , i.e. $r$ is a root of $\chi(x) = x^2 - px - q$ (for $r \ne 0$ ).

Proof

$r^{n+2} - p\,r^{n+1} - q\,r^n = r^n \chi(r)$ . If $\chi(r) = 0$ this is $0$ for every $n$ . Conversely, if it is $0$ for $n = 0$ , then $\chi(r) = 0$ .

∎

Theorem— Theorem 1 (distinct roots)

If $\chi(x) = x^2 - px - q$ has two distinct roots $r \ne s$ (possibly complex), then the solutions of $a_{n+2} = p\,a_{n+1} + q\,a_n$ are exactly the sequences $a_n = A r^n + B s^n$ , where

A = \frac{a_1 - s\,a_0}{r - s}, \qquad B = \frac{r\,a_0 - a_1}{r - s}.

Proof

By Lemmas 1 and 3, $b_n = A r^n + B s^n$ is a solution for every $A, B$ . With the given $A, B$ we have $b_0 = A + B = \frac{(r - s) a_0}{r - s} = a_0$ and $b_1 = A r + B s = \frac{r a_1 - rs\,a_0 + rs\,a_0 - s a_1}{r - s} = a_1$ . By Lemma 2, $a_n = b_n$ for all $n$ .

∎

Theorem— Theorem 2 (a repeated root)

If $\chi(x) = (x - r)^2$ with $r \ne 0$ , i.e. $p = 2r$ and $q = -r^2$ , then the solutions are exactly the sequences $a_n = (A + Bn)\,r^n$ .

Proof

First, $n r^n$ is a solution: $(n+2)r^{n+2} - 2r(n+1)r^{n+1} + r^2 \cdot n r^n = r^{n+2}\big((n+2) - 2(n+1) + n\big) = 0$ . So every $(A + Bn)r^n$ is a solution by Lemma 1. Its initial values are $A$ and $(A + B)r$ ; since $r \ne 0$ , any prescribed $a_0, a_1$ are matched by $A = a_0$ , $B = a_1/r - a_0$ . Lemma 2 finishes the proof.

∎

Theorem— Corollary (Binet's formula)

With $F_0 = 0$ , $F_1 = 1$ , $F_{n+2} = F_{n+1} + F_n$ , and $\varphi = \frac{1 + \sqrt5}{2}$ , $\psi = \frac{1 - \sqrt5}{2}$ ,

F_n = \frac{\varphi^n - \psi^n}{\sqrt5} \qquad (n \ge 0).

Moreover $F_n$ is the integer nearest to $\varphi^n/\sqrt5$ .

Proof

The roots of $x^2 - x - 1$ are $\varphi \ne \psi$ , with $\varphi - \psi = \sqrt5$ . Theorem 1 with $a_0 = 0$ , $a_1 = 1$ gives $A = \frac{1}{\sqrt5}$ and $B = -\frac{1}{\sqrt5}$ . For the second claim, $|\psi| \approx 0.618 < 1$ , so $|\psi^n/\sqrt5| \le 1/\sqrt5 < \tfrac12$ .

∎

The formula is remarkable: an integer sequence, expressed through irrational numbers whose irrational parts cancel exactly.

The general theorem. For order $k$ , factor $\chi(x) = \prod_{i}(x - r_i)^{m_i}$ over $\C$ with distinct roots $r_i \ne 0$ . Then the solutions are exactly

a_n = \sum_i P_i(n)\, r_i^n, \qquad P_i \text{ a polynomial of degree less than } m_i .

Lemmas 1–3 generalise word for word; the remaining work is to check that $n^j r_i^n$ ( $j < m_i$ ) are solutions and that these $k$ sequences are linearly independent. The generating-function proof in the next section does both at once.

Inhomogeneous recurrences. If $(b_n)$ is one solution of $a_{n+k} = c_1 a_{n+k-1} + \cdots + c_k a_n + g(n)$ , then every solution is $b_n + h_n$ with $(h_n)$ a solution of the homogeneous recurrence — the difference of two solutions solves the homogeneous one. A particular solution can often be guessed in the shape of $g$ : for $a_{n+1} = 2a_n + 1$ try a constant, $b_n = -1$ ; for $a_{n+1} = 2a_n + n$ try $b_n = \alpha n + \beta$ , giving $\alpha = -1$ , $\beta = -1$ . (When the guess shape is itself a homogeneous solution, multiply it by $n$ , exactly as for differential equations.)

ProofH

Generating functions

Theorem— Proposition (inverses in K[[x]])

A formal power series $A(x) = \sum a_n x^n$ has a multiplicative inverse in $K[[x]]$ if and only if $a_0 \ne 0$ .

Proof

If $A B = 1$ then comparing constant terms gives $a_0 b_0 = 1$ , so $a_0 \ne 0$ . Conversely, if $a_0 \ne 0$ we solve $AB = 1$ coefficient by coefficient: $b_0 = 1/a_0$ , and for $n \ge 1$ the equation $\sum_{i=0}^{n} a_i b_{n-i} = 0$ determines $b_n = -\frac{1}{a_0}\sum_{i=1}^{n} a_i b_{n-i}$ from $b_0, \dots, b_{n-1}$ .

∎

For example $(1 - x)(1 + x + x^2 + \cdots) = 1$ , so $\frac{1}{1 - x} = \sum_{n \ge 0} x^n$ as an identity of formal power series — true whatever " $x$ " is, because it is a statement about coefficients. More generally, for a constant $r$ , $\frac{1}{1 - rx} = \sum r^n x^n$ , and differentiating formally (or expanding),

\frac{1}{(1 - rx)^m} = \sum_{n \ge 0} \binom{n + m - 1}{m - 1} r^n x^n .

The coefficient is a polynomial in $n$ of degree $m - 1$ , times $r^n$ .

Theorem— Theorem 3 (rational generating functions)

Let $Q(x) = 1 - c_1 x - c_2 x^2 - \cdots - c_k x^k$ . A sequence satisfies $a_{n+k} = c_1 a_{n+k-1} + \cdots + c_k a_n$ for all $n \ge 0$ if and only if its generating function is $A(x) = P(x)/Q(x)$ for a polynomial $P$ of degree less than $k$ .

Proof

The coefficient of $x^{n+k}$ in $Q(x)A(x)$ is $a_{n+k} - c_1 a_{n+k-1} - \cdots - c_k a_n$ . So the recurrence holds for all $n \ge 0$ if and only if $Q(x)A(x)$ has no terms of degree $\ge k$ , i.e. $Q A = P$ is a polynomial of degree less than $k$ . Since $Q$ has constant term $1$ , it is invertible, and $QA = P \iff A = P/Q$ .

∎

Note that $Q(x) = x^k\chi(1/x)$ : the characteristic polynomial written backwards. So if $\chi(x) = \prod (x - r_i)^{m_i}$ then $Q(x) = \prod (1 - r_i x)^{m_i}$ , and partial fractions write $P/Q$ as a sum of terms $\frac{\beta}{(1 - r_i x)^j}$ with $j \le m_i$ . By the expansion above, the coefficient of $x^n$ in each term is a polynomial in $n$ of degree less than $m_i$ times $r_i^n$ — which proves the general characteristic-root theorem. Every solution has this form; conversely every such sequence has a generating function $P/Q$ , hence solves the recurrence.

Example— Fibonacci, again

With $c_1 = c_2 = 1$ and $F_0 = 0$ , $F_1 = 1$ : $P(x) = F_0 + (F_1 - F_0)x = x$ , so

F(x) = \frac{x}{1 - x - x^2} = \frac{x}{(1 - \varphi x)(1 - \psi x)} = \frac{1}{\sqrt5}\left(\frac{1}{1 - \varphi x} - \frac{1}{1 - \psi x}\right),

using $\varphi + \psi = 1$ , $\varphi\psi = -1$ and $\varphi - \psi = \sqrt5$ . Reading off the coefficient of $x^n$ gives Binet's formula a second time.

Counting with products. Generating functions turn combinatorial constructions into algebra. If $A(x) = \sum a_n x^n$ counts objects of one kind by size and $B(x)$ another, then the coefficient of $x^n$ in $A(x)B(x)$ is $\sum_i a_i b_{n-i}$ : the number of pairs of total size $n$ . A choice repeated any number of times corresponds to $\frac{1}{1 - A(x)}$ (when $a_0 = 0$ ).

Example— Paying with coins

In how many ways can a shopkeeper in Chennai make $10$ rupees from coins of $1$ , $2$ and $5$ rupees? Choosing how many coins of each kind is choosing a pair, then a triple, so the answer is the coefficient of $x^{10}$ in

\frac{1}{(1 - x)(1 - x^2)(1 - x^5)} = (1 + x + x^2 + \cdots)(1 + x^2 + x^4 + \cdots)(1 + x^5 + x^{10} + \cdots).

Group by the number of five-rupee coins: with none, $10$ rupees from $1$ s and $2$ s ( $6$ ways: zero to five $2$ s); with one, $5$ rupees ( $3$ ways); with two, $1$ way. Total $10$ .

Example— Compositions

A composition of $n$ into parts $1$ and $2$ is a sequence of $1$ s and $2$ s with sum $n$ — a rhythm, in the language of the motivation. One part has generating function $x + x^2$ , so sequences of parts have $\frac{1}{1 - x - x^2} = \sum F_{n+1}x^n$ . The rhythm count $t_n = F_{n+1}$ falls out without any recurrence.

ProofH

Catalan numbers

A Dyck path of semilength $n$ is a sequence of $n$ up-steps $U = (1, 1)$ and $n$ down-steps $D = (1, -1)$ , starting at height $0$ and never going below height $0$ . Reading $U$ as "(" and $D$ as ")" identifies Dyck paths with balanced bracket sequences of $n$ pairs. Let $C_n$ be their number: $C_0 = 1$ , $C_1 = 1$ (()), $C_2 = 2$ ((()), ()()), $C_3 = 5$ .

Theorem— Proposition (Segner's recurrence)

$C_{n+1} = \sum_{i=0}^{n} C_i\,C_{n-i}$ for $n \ge 0$ .

Proof

Every non-empty balanced sequence starts with "(", and that bracket is closed at a unique matching ")": the sequence is $(\,X\,)\,Y$ with $X$ and $Y$ balanced. If $X$ has $i$ pairs then $Y$ has $n - i$ , and the decomposition is a bijection, so $C_{n+1} = \sum_i C_i C_{n-i}$ .

∎

Theorem— Theorem 4 (the Catalan formula)

C_n = \binom{2n}{n} - \binom{2n}{n+1} = \frac{1}{n+1}\binom{2n}{n}.

Proof

(The reflection argument.) There are $\binom{2n}{n}$ paths from $(0, 0)$ to $(2n, 0)$ with $n$ up- and $n$ down-steps. Call such a path bad if it touches height $-1$ . For a bad path, reflect the part before its first visit to height $-1$ in the line $y = -1$ . The result is a path from $(0, -2)$ to $(2n, 0)$ . Conversely, every path from $(0, -2)$ to $(2n, 0)$ must cross height $-1$ ; reflecting its part before the first visit gives back a bad path. So bad paths are in bijection with paths from height $-2$ to height $0$ in $2n$ steps, which have $n + 1$ up-steps and $n - 1$ down-steps: there are $\binom{2n}{n+1}$ of them. Hence

C_n = \binom{2n}{n} - \binom{2n}{n+1} = \binom{2n}{n}\left(1 - \frac{n}{n+1}\right) = \frac{1}{n+1}\binom{2n}{n},

since $\binom{2n}{n+1} = \binom{2n}{n}\frac{n}{n+1}$ .

∎

A second proof, by generating functions. Let $C(x) = \sum C_n x^n$ . Segner's recurrence says exactly that $C(x) = 1 + x\,C(x)^2$ . Multiplying by $4x$ and completing the square, $(1 - 2x\,C(x))^2 = 1 - 4x$ . In $\Q[[x]]$ the series $1 - 4x$ has exactly two square roots, $\pm S(x)$ , where $S$ is the unique square root with constant term $1$ (its coefficients are found one at a time, as for inverses). Since $1 - 2xC(x)$ has constant term $1$ , $1 - 2x\,C(x) = S(x) = \sqrt{1 - 4x}$ . The binomial series $\sqrt{1 - 4x} = \sum_n \binom{1/2}{n}(-4)^n x^n = 1 - 2\sum_{n \ge 1} \frac{1}{n}\binom{2n-2}{n-1}x^n$ (it has constant term $1$ , and its square is $1 - 4x$ by Vandermonde's identity $\sum_i \binom{a}{i}\binom{b}{n-i} = \binom{a+b}{n}$ , a polynomial identity in $a$ and $b$ ) then gives

C(x) = \frac{1 - \sqrt{1 - 4x}}{2x}, \qquad C_n = \frac{1}{n+1}\binom{2n}{n}.

(The identity $\binom{1/2}{n}(-4)^n = -\frac{2}{n}\binom{2n-2}{n-1}$ for $n \ge 1$ is a direct computation with $\binom{1/2}{n} = \frac{\frac12(\frac12 - 1)\cdots(\frac12 - n + 1)}{n!}$ .) Every step is algebra in $\Q[[x]]$ ; that the series also converges for $|x| < \tfrac14$ is a bonus, not a requirement.

The Catalan numbers $1, 1, 2, 5, 14, 42, 132, 429, \dots$ count well over two hundred families of objects (Stanley's monograph lists 214), among them triangulations of a convex $(n+2)$ -gon, binary trees with $n$ internal nodes, ways to bracket a product of $n + 1$ factors, and non-crossing handshakes among $2n$ people seated at a round table.

ProofH

How fast does it grow?

Exact formulas are not always available, and not always wanted: an engineer choosing between two algorithms needs to know that one takes about $n^2$ steps and the other about $n \log n$ , not the exact counts. Asymptotic notation says this precisely.

Example— Using the definitions

$3n^2 + 5n = \Theta(n^2)$ : for $n \ge 1$ , $3n^2 \le 3n^2 + 5n \le 8n^2$ . The constants $3$ and $8$ and the threshold $1$ are the witnesses.
$n^2 = O(n^3)$ , but $n^3 \ne O(n^2)$ : $n^3 / n^2 = n$ is unbounded.
$2^{n+1} = \Theta(2^n)$ , but $4^n \ne O(2^n)$ : constant factors are hidden, but a change of base is not.
$\log_2 n = \Theta(\ln n)$ , since $\log_2 n = \ln n / \ln 2$ . So the base of a logarithm inside $O$ does not matter.
$F_n = \Theta(\varphi^n)$ and in fact $F_n \sim \varphi^n/\sqrt5$ , by Binet's formula.

Theorem— Proposition (the scale of growth)

For every $k \ge 0$ , $\varepsilon > 0$ and $r > 1$ : $\ \ln n = o(n^\varepsilon)$ , $\ n^k = o(r^n)$ and $r^n = o(n!)$ .

Proof

For $n^k = o(r^n)$ : the ratio $u_n = n^k/r^n$ satisfies $u_{n+1}/u_n = (1 + 1/n)^k / r \to 1/r < 1$ , so from some point on $u_{n+1} \le \rho\, u_n$ with $\rho = (1 + 1/r)/2 < 1$ , and $u_n \to 0$ geometrically. For $r^n = o(n!)$ : $r^n/n! = \prod_{j=1}^{n} (r/j)$ , and every factor with $j \ge 2r$ is at most $\tfrac12$ . For $\ln n = o(n^\varepsilon)$ : put $n = e^{t}$ ; then $\ln n / n^\varepsilon = t/e^{\varepsilon t}$ , which tends to $0$ as $t \to \infty$ (for instance by L'Hôpital's rule).

∎

Precise asymptotics often need analysis. Stirling's formula $n! \sim \sqrt{2\pi n}\,(n/e)^n$ gives

C_n = \frac{(2n)!}{(n+1)!\,n!} \sim \frac{4^n}{\sqrt{\pi}\, n^{3/2}},

which the second experiment below checks numerically.

Divide-and-conquer recurrences. Mergesort sorts $n$ items by sorting two halves and merging them with at most $n - 1$ comparisons. Its cost satisfies $T(n) = 2T(n/2) + n$ (up to rounding and lower-order terms). These recurrences jump back by a factor, so the characteristic method does not apply directly — but on powers of two they become linear.

Theorem— Proposition (unrolling)

If $T(1) = 0$ and $T(n) = 2T(n/2) + n$ for $n = 2, 4, 8, \dots$ , then $T(2^k) = k\,2^k$ , i.e. $T(n) = n\log_2 n$ for $n$ a power of two.

Proof

Put $u_k = T(2^k)/2^k$ . Dividing $T(2^{k+1}) = 2T(2^k) + 2^{k+1}$ by $2^{k+1}$ gives $u_{k+1} = u_k + 1$ , with $u_0 = 0$ . So $u_k = k$ .

∎

Picture the recursion as a tree: level $j$ has $2^j$ subproblems of size $n/2^j$ , costing $n$ in total, and there are $\log_2 n$ levels. The general pattern is the master theorem (Bentley, Haken and Saxe, 1980), stated here without proof (see Cormen et al., §4.5): for $T(n) = a\,T(n/b) + f(n)$ with $a \ge 1$ , $b > 1$ , put $c^* = \log_b a$ ; then

if $f(n) = O(n^{c})$ for some $c < c^*$ , then $T(n) = \Theta(n^{c^*})$ — the leaves dominate;
if $f(n) = \Theta(n^{c^*})$ , then $T(n) = \Theta(n^{c^*}\log n)$ — every level costs the same (mergesort: $a = b = 2$ );
if $f(n) = \Omega(n^{c})$ for some $c > c^*$ and $a f(n/b) \le \delta f(n)$ for some $\delta < 1$ and all large $n$ , then $T(n) = \Theta(f(n))$ — the root dominates.

Karatsuba's multiplication, $T(n) = 3T(n/2) + O(n)$ , lands in the first case: $\Theta(n^{\log_2 3}) \approx \Theta(n^{1.585})$ , beating the schoolbook $n^2$ . Recurrences of this kind are the bread and butter of algorithm design.

Formal mathematicsF

Recurrences in Lean and Mathlib

The Lean module follows the lesson's proofs. First, what it means to solve the recurrence $a_{n+2} = p\,a_{n+1} + q\,a_n$ , and Lemmas 1–3 — notice that Lemma 2's induction carries the pair of statements a n = b n ∧ a (n + 1) = b (n + 1), exactly as in the human proof:

IsSolLean 4Formally verified

/-- `IsSol p q a` says that the real sequence `a` satisfies the second-order linear recurrence
with constant coefficients `aₙ₊₂ = p · aₙ₊₁ + q · aₙ` for every `n`. Its characteristic
polynomial is `x² − p x − q`. -/
def IsSol (p q : ℝ) (a : ℕ → ℝ) : Prop :=
  ∀ n, a (n + 2) = p * a (n + 1) + q * a n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

isSol_geomLean 4Proved here from basic factsFormally verified

/-- **Guess an exponential.** If `r` is a root of the characteristic polynomial, `r² = p r + q`,
then `aₙ = rⁿ` solves the recurrence: `rⁿ⁺² = rⁿ · r² = rⁿ (p r + q) = p rⁿ⁺¹ + q rⁿ`. -/
theorem isSol_geom {p q r : ℝ} (hr : r ^ 2 = p * r + q) : IsSol p q (fun n => r ^ n) := by
  intro n
  calc r ^ (n + 2) = r ^ n * r ^ 2 := by ring
    _ = r ^ n * (p * r + q) := by rw [hr]
    _ = p * r ^ (n + 1) + q * r ^ n := by ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

isSol_add_smulLean 4Proved here from basic factsFormally verified

/-- **Linearity.** If `a` and `b` solve the recurrence, so does every combination `A a + B b`.
So the solutions form a vector space. -/
theorem isSol_add_smul {p q : ℝ} {a b : ℕ → ℝ} (ha : IsSol p q a) (hb : IsSol p q b)
    (A B : ℝ) : IsSol p q (fun n => A * a n + B * b n) := by
  intro n
  simp only
  rw [ha n, hb n]
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

isSol_uniqueLean 4Proved here from basic factsFormally verified

/-- **Two initial values determine a solution.** If `a` and `b` solve the same recurrence and
agree at `0` and `1`, they agree everywhere. The induction carries *two* consecutive values at
once: from `aₙ = bₙ` and `aₙ₊₁ = bₙ₊₁` the recurrence gives `aₙ₊₂ = bₙ₊₂`. -/
theorem isSol_unique {p q : ℝ} {a b : ℕ → ℝ} (ha : IsSol p q a) (hb : IsSol p q b)
    (h0 : a 0 = b 0) (h1 : a 1 = b 1) : ∀ n, a n = b n := by
  have key : ∀ n, a n = b n ∧ a (n + 1) = b (n + 1) := by
    intro n
    induction n with
    | zero => exact ⟨h0, h1⟩
    | succ k ih =>
      refine ⟨ih.2, ?_⟩
      rw [ha k, hb k, ih.1, ih.2]
  exact fun n => (key n).1

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

Theorem 1 is assembled from the lemmas, and Theorem 2's extra solution $n r^n$ is a one-line computation:

distinct_rootsLean 4Proved here from basic factsFormally verified

/-- **The characteristic-root theorem (distinct roots).** If `r ≠ s` are roots of
`x² − p x − q`, every solution has the form `aₙ = A rⁿ + B sⁿ`, with `A` and `B` fixed by the
initial values: `A = (a₁ − s a₀)/(r − s)` and `B = (r a₀ − a₁)/(r − s)`.
Proof: the right-hand side solves the recurrence (`isSol_geom`, `isSol_add_smul`) and has the
right values at `0` and `1`, so it equals `a` by `isSol_unique`. -/
theorem distinct_roots {p q r s : ℝ} (hrs : r ≠ s) (hr : r ^ 2 = p * r + q)
    (hs : s ^ 2 = p * s + q) {a : ℕ → ℝ} (ha : IsSol p q a) (n : ℕ) :
    a n = (a 1 - s * a 0) / (r - s) * r ^ n + (r * a 0 - a 1) / (r - s) * s ^ n := by
  have hne : r - s ≠ 0 := sub_ne_zero.mpr hrs
  refine isSol_unique ha (isSol_add_smul (isSol_geom hr) (isSol_geom hs) _ _) ?_ ?_ n
  · field_simp
    ring
  · field_simp
    ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

isSol_repeatedLean 4Proved here from basic factsFormally verified

/-- **A repeated root.** If the characteristic polynomial is `(x − r)² = x² − 2r x + r²`, then
besides `rⁿ` the sequence `n rⁿ` is a solution of `aₙ₊₂ = 2r aₙ₊₁ − r² aₙ`. -/
theorem isSol_repeated (r : ℝ) : IsSol (2 * r) (-r ^ 2) (fun n => (n : ℝ) * r ^ n) := by
  intro n
  push_cast
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

three_pow_isSolLean 4Proved here from basic factsFormally verified

/-- `aₙ = 3ⁿ` solves `aₙ₊₂ = 5aₙ₊₁ − 6aₙ`, because `3` is a root of `x² − 5x + 6 = (x − 2)(x − 3)`:
`3² = 5 · 3 − 6`. An instance of `isSol_geom`. -/
theorem three_pow_isSol : IsSol 5 (-6) (fun n => (3 : ℝ) ^ n) :=
  isSol_geom (by norm_num)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

Binet's formula then follows from Theorem 1 exactly as in the corollary. Mathlib already has it, as Real.coe_fib_eq, and also a general theory of linear recurrences of any order (LinearRecurrence), including the dimension of the solution space and "guess an exponential":

fib_isSolLean 4Proved here from basic factsFormally verified

/-- The Fibonacci numbers (Mathlib's `Nat.fib`, with `F₀ = 0`, `F₁ = 1`) solve
`Fₙ₊₂ = Fₙ₊₁ + Fₙ`, i.e. `IsSol 1 1`. -/
theorem fib_isSol : IsSol 1 1 (fun n => (Nat.fib n : ℝ)) := by
  intro n
  simp only [one_mul]
  rw [Nat.fib_add_two, Nat.cast_add, add_comm]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

binetLean 4Proved here from basic factsFormally verified

/-- **Binet's formula**, `Fₙ = (φⁿ − ψⁿ)/√5` with `φ = (1 + √5)/2` and `ψ = (1 − √5)/2`, proved
as in the lesson: `φ` and `ψ` are the distinct roots of `x² − x − 1`, so `distinct_roots`
applies with `F₀ = 0` and `F₁ = 1`, and `φ − ψ = √5`. -/
theorem binet (n : ℕ) : (Nat.fib n : ℝ) = (goldenRatio ^ n - goldenConj ^ n) / √5 := by
  have hφ : goldenRatio ^ 2 = 1 * goldenRatio + 1 := by rw [goldenRatio_sq]; ring
  have hψ : goldenConj ^ 2 = 1 * goldenConj + 1 := by rw [goldenConj_sq]; ring
  have hne : goldenRatio ≠ goldenConj := by
    intro h
    have : goldenRatio - goldenConj = 0 := by rw [h, sub_self]
    rw [goldenRatio_sub_goldenConj] at this
    exact absurd this (by positivity)
  rw [distinct_roots hne hφ hψ fib_isSol n, goldenRatio_sub_goldenConj]
  simp only [Nat.fib_zero, Nat.fib_one, Nat.cast_zero, Nat.cast_one, mul_zero, sub_zero,
    zero_sub]
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

binet_libraryLean 4Applies a library theoremFormally verified

/-- Binet's formula as it appears in Mathlib: `Real.coe_fib_eq`. Mathlib proves it with its
general `LinearRecurrence` theory, the same argument as `binet` above. -/
theorem binet_library (n : ℕ) : (Nat.fib n : ℝ) = (goldenRatio ^ n - goldenConj ^ n) / √5 :=
  Real.coe_fib_eq n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

geom_sol_iff_rootLean 4Applies a library theoremFormally verified

/-- Mathlib's version of "guess an exponential", for a linear recurrence `E` of any order over
a commutative ring without zero divisors: `qⁿ` is a solution exactly when `q` is a root of the
characteristic polynomial. This applies `LinearRecurrence.geom_sol_iff_root_charPoly`. -/
theorem geom_sol_iff_root (E : LinearRecurrence ℝ) (q : ℝ) :
    E.IsSolution (fun n => q ^ n) ↔ E.charPoly.IsRoot q :=
  E.geom_sol_iff_root_charPoly q

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

Two recurrences from algorithms. The divide-and-conquer recurrence is defined by well-founded recursion — Lean demands a proof that $\lfloor n/2 \rfloor < n$ before it accepts the definition, a small reminder that a recurrence only defines something if it terminates:

hanoiLean 4Formally verified

/-- The number of moves the recursive solution of the Tower of Hanoi makes with `n` discs:
move `n − 1` discs aside, move the largest disc, move the `n − 1` discs back on top. -/
def hanoi : ℕ → ℕ
  | 0 => 0
  | n + 1 => 2 * hanoi n + 1

Axioms used: No axiomsformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

hanoi_eqLean 4Proved here from basic factsFormally verified

/-- The Hanoi recurrence `Hₙ₊₁ = 2Hₙ + 1`, `H₀ = 0` has solution `Hₙ = 2ⁿ − 1`, stated without
subtraction as `Hₙ + 1 = 2ⁿ`: adding `1` turns the recurrence into `Hₙ₊₁ + 1 = 2 (Hₙ + 1)`. -/
theorem hanoi_eq (n : ℕ) : hanoi n + 1 = 2 ^ n := by
  induction n with
  | zero => rfl
  | succ k ih =>
    calc hanoi (k + 1) + 1 = 2 * (hanoi k + 1) := by simp only [hanoi]; ring
      _ = 2 ^ (k + 1) := by rw [ih]; ring

Axioms used: propextformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

splitCostLean 4Formally verified

/-- The cost recurrence of a divide-and-conquer algorithm such as mergesort, with the halves
rounded down: `T(n) = 2 T(⌊n/2⌋) + n` for `n ≥ 2`, and `T(0) = T(1) = 0`. Lean accepts the
definition because `⌊n/2⌋ < n` when `n ≥ 2` (checked by `omega`). -/
def splitCost (n : ℕ) : ℕ :=
  if n ≤ 1 then 0 else 2 * splitCost (n / 2) + n
decreasing_by omega

Axioms used: propext, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

splitCost_pow_twoLean 4Proved here from basic factsFormally verified

/-- **Unrolling a divide-and-conquer recurrence.** On powers of two, `T(2ᵏ) = k · 2ᵏ`: each of
the `k` levels of the recursion costs `2ᵏ` in total. So `T(n) = n log₂ n` when `n = 2ᵏ`. -/
theorem splitCost_pow_two (k : ℕ) : splitCost (2 ^ k) = k * 2 ^ k := by
  induction k with
  | zero => simp [splitCost]
  | succ k ih =>
    have hgt : ¬ 2 ^ (k + 1) ≤ 1 := by
      have : 2 ≤ 2 ^ (k + 1) := by
        calc 2 = 2 ^ 1 := rfl
          _ ≤ 2 ^ (k + 1) := Nat.pow_le_pow_right (by norm_num) (by omega)
      omega
    have hhalf : 2 ^ (k + 1) / 2 = 2 ^ k := by rw [pow_succ]; simp
    rw [splitCost]
    simp only [hgt, ite_false]
    rw [hhalf, ih]
    ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

Formal power series. Mathlib's PowerSeries ℚ, written ℚ⟦X⟧, is literally the ring of the definitions section: a power series is a function from exponents to coefficients, and PowerSeries.coeff n reads off a coefficient. The Fibonacci generating function is verified coefficient by coefficient — and the factorial series, which converges nowhere except at $0$ , is nevertheless invertible:

geometric_seriesLean 4Applies a library theoremFormally verified

/-- **The geometric series as an identity of formal power series**: in `ℚ⟦X⟧`,
`(1 + X + X² + ⋯)(1 − X) = 1`. No convergence is involved: the coefficients of the product are
finite sums. This applies Mathlib's `PowerSeries.mk_one_mul_one_sub_eq_one`. -/
theorem geometric_series : (mk 1 : ℚ⟦X⟧) * (1 - X) = 1 :=
  mk_one_mul_one_sub_eq_one ℚ

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

fib_gfLean 4Proved here from basic factsFormally verified

/-- **The generating function of the Fibonacci numbers.** With `F(X) = Σ Fₙ Xⁿ` in `ℚ⟦X⟧`,
`(1 − X − X²) F(X) = X`, i.e. `F(X) = X / (1 − X − X²)`. Coefficient by coefficient: the
coefficient of `Xⁿ⁺²` is `Fₙ₊₂ − Fₙ₊₁ − Fₙ = 0`, and those of `1` and `X` are `F₀ = 0` and
`F₁ − F₀ = 1`. -/
theorem fib_gf :
    (1 - X - X ^ 2 : ℚ⟦X⟧) * mk (fun n => (Nat.fib n : ℚ)) = X := by
  ext n
  rw [sub_mul, sub_mul, one_mul, map_sub, map_sub, coeff_mk]
  rcases n with _ | _ | n
  · simp
  · simp [coeff_X, pow_two, mul_assoc]
  · rw [pow_two, mul_assoc, coeff_succ_X_mul, coeff_succ_X_mul, coeff_succ_X_mul, coeff_mk,
      coeff_mk, coeff_X, Nat.fib_add_two]
    simp only [Nat.cast_add, show n + 1 + 1 ≠ 1 by omega, ite_false]
    ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

factorial_series_isUnitLean 4Proved here from basic factsFormally verified

/-- **A formal power series need not converge to be useful.** The series `Σ n! Xⁿ` converges
only at `X = 0`, yet it is invertible in `ℚ⟦X⟧`, because its constant term `0! = 1` is
invertible (Mathlib's criterion `PowerSeries.isUnit_iff_constantCoeff`). -/
theorem factorial_series_isUnit : IsUnit (mk (fun n => (Nat.factorial n : ℚ))) := by
  rw [isUnit_iff_constantCoeff, ← coeff_zero_eq_constantCoeff_apply, coeff_mk]
  simp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

Catalan numbers. Mathlib defines catalan by Segner's recurrence and proves the closed form:

catalan_formulaLean 4Applies a library theoremFormally verified

/-- **The Catalan formula** `Cₙ = C(2n, n)/(n + 1)`. Mathlib *defines* `catalan` by Segner's
recurrence `Cₙ₊₁ = Σᵢ Cᵢ Cₙ₋ᵢ` (`catalan_succ`) and proves this closed form in
`catalan_eq_centralBinom_div`; `Nat.centralBinom n` is `C(2n, n)`, and the division is exact. -/
theorem catalan_formula (n : ℕ) : catalan n = n.centralBinom / (n + 1) :=
  catalan_eq_centralBinom_div n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

catalan_fiveLean 4Proved here from basic factsFormally verified

/-- A computation: `C₅ = 42` (the number of balanced strings of five pairs of brackets, and of
triangulations of a convex heptagon), evaluated from the closed form `C(10, 5)/6 = 252/6`. -/
theorem catalan_five : catalan 5 = 42 := by
  rw [catalan_formula]
  decide

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

Asymptotics. Mathlib's f =O[atTop] g is the definition of the lesson, phrased with filters: "eventually, $\|f(n)\| \le C\|g(n)\|$ ". The first proof supplies the witnesses $C = 8$ and $N = 1$ ; the second uses $F_n \le \varphi^n$ , itself proved by a two-step induction:

quadratic_isBigOLean 4Proved here from basic factsFormally verified

/-- `3n² + 5n = O(n²)`: for `n ≥ 1`, `5n ≤ 5n²`, so `3n² + 5n ≤ 8n²`. The constant `8` and the
threshold `1` are witnesses; big-O hides both. -/
theorem quadratic_isBigO :
    (fun n : ℕ => (3 * (n : ℝ) ^ 2 + 5 * n)) =O[atTop] (fun n : ℕ => (n : ℝ) ^ 2) := by
  refine IsBigO.of_bound 8 ?_
  filter_upwards [eventually_ge_atTop 1] with n hn
  have hn' : (1 : ℝ) ≤ n := by exact_mod_cast hn
  have h0 : (0 : ℝ) ≤ n := by linarith
  rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (by positivity),
    abs_of_nonneg (by positivity)]
  nlinarith

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

fib_le_gold_powLean 4Proved here from basic factsFormally verified

/-- `Fₙ ≤ φⁿ` for every `n`, by a two-step induction that uses only `φ² = φ + 1`:
`Fₙ₊₂ = Fₙ₊₁ + Fₙ ≤ φⁿ⁺¹ + φⁿ = φⁿ (φ + 1) = φⁿ⁺²`. -/
theorem fib_le_gold_pow (n : ℕ) : (Nat.fib n : ℝ) ≤ goldenRatio ^ n := by
  have key : ∀ n, (Nat.fib n : ℝ) ≤ goldenRatio ^ n ∧
      (Nat.fib (n + 1) : ℝ) ≤ goldenRatio ^ (n + 1) := by
    intro n
    induction n with
    | zero => simp [one_lt_goldenRatio.le]
    | succ k ih =>
      refine ⟨ih.2, ?_⟩
      calc (Nat.fib (k + 2) : ℝ) = Nat.fib (k + 1) + Nat.fib k := by
            rw [Nat.fib_add_two, Nat.cast_add, add_comm]
        _ ≤ goldenRatio ^ (k + 1) + goldenRatio ^ k := add_le_add ih.2 ih.1
        _ = goldenRatio ^ k * (goldenRatio + 1) := by ring
        _ = goldenRatio ^ (k + 2) := by rw [← goldenRatio_sq]; ring
  exact (key n).1

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

fib_isBigOLean 4Proved here from basic factsFormally verified

/-- `Fₙ = O(φⁿ)`, from `fib_le_gold_pow` with constant `1`. (Binet's formula shows more:
`Fₙ = Θ(φⁿ)`, since `|ψⁿ| ≤ 1`.) -/
theorem fib_isBigO :
    (fun n : ℕ => (Nat.fib n : ℝ)) =O[atTop] (fun n : ℕ => goldenRatio ^ n) := by
  refine IsBigO.of_bound 1 (Eventually.of_forall fun n => ?_)
  rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (by positivity),
    abs_of_nonneg (by positivity), one_mul]
  exact fib_le_gold_pow n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

poly_isLittleO_expLean 4Applies a library theoremFormally verified

/-- **Polynomials lose to exponentials**: `nᵏ = o(rⁿ)` for every `k` and every `r > 1`. This
applies Mathlib's `isLittleO_pow_const_const_pow_of_one_lt`. -/
theorem poly_isLittleO_exp (k : ℕ) {r : ℝ} (hr : 1 < r) :
    (fun n : ℕ => (n : ℝ) ^ k) =o[atTop] (fun n : ℕ => r ^ n) :=
  isLittleO_pow_const_const_pow_of_one_lt k hr

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RecurrencesGeneratingFunctions.leanTry it in the Lean web editor

What is and is not formalised. Proved here: Lemmas 1–3, Theorem 1, the extra solution in Theorem 2 (not the full "exactly these" statement), Binet's formula, $F_n \le \varphi^n$ , the Hanoi formula, $T(2^k) = k\,2^k$ , the Fibonacci generating function, and two big-O facts. Cited from Mathlib: the general-order theory of linear recurrences, the geometric series in $K[[x]]$ , the invertibility criterion, the Catalan closed form and $n^k = o(r^n)$ . Not formalised: partial fractions, the reflection proof, the generating-function proof of the Catalan formula, Stirling-type asymptotics and the master theorem.

ComputationC

Experiments: four routes to Fibonacci, four routes to Catalan

The first experiment computes Fibonacci numbers from the recurrence, from the generating function $x/(1 - x - x^2)$ by exact power-series division, and by repeated squaring of the matrix $\begin{pmatrix} 1 & 1 \\ 1 & 0 \end{pmatrix}$ , and checks that they agree. Then it evaluates Binet's formula in floating point and finds where the rounded answer first goes wrong. The formula is a theorem; its floating-point evaluation is not — a theme of numerical methods.

Fibonacci numbers: recurrence, Binet, generating function, matricesPythonExact computationNumerical approximationExhaustive finite checkComputationally tested

"""Three ways to compute Fibonacci numbers, and where floating point fails.

The recurrence F(n+2) = F(n+1) + F(n) gives exact integers. Binet's formula
F(n) = (phi^n - psi^n)/sqrt(5) is an exact theorem, but evaluating it with
64-bit floats is not exact: phi and sqrt(5) are rounded, and once F(n) has
more than about 16 significant digits the rounded answer must go wrong. The
generating function x/(1 - x - x^2) gives the same numbers again, by dividing
power series exactly. Finally, the matrix identity
[[1, 1], [1, 0]]^n = [[F(n+1), F(n)], [F(n), F(n-1)]] computes F(n) with only
about log2(n) matrix multiplications, and its determinant gives Cassini's
identity F(n+1)F(n-1) - F(n)^2 = (-1)^n.
"""

import math

def fib_list(count):
    """The first `count` Fibonacci numbers F(0), F(1), ..., exactly."""
    out = []
    a, b = 0, 1
    for _ in range(count):
        out.append(a)
        a, b = b, a + b
    return out

def series_divide(num, den, count):
    """First `count` coefficients of num(x)/den(x) as a formal power series.

    `num` and `den` are coefficient lists; den[0] must be 1 so that only
    integer arithmetic is needed. Coefficient n is found from
    num[n] = sum(den[k] * q[n - k]), solved for q[n].
    """
    if not den or den[0] != 1:
        raise ValueError("the denominator must have constant term 1")
    q = []
    for n in range(count):
        c = num[n] if n < len(num) else 0
        for k in range(1, min(n, len(den) - 1) + 1):
            c -= den[k] * q[n - k]
        q.append(c)
    return q

def mat_mul(x, y):
    """Product of 2 x 2 integer matrices given as ((a, b), (c, d))."""
    (a, b), (c, d) = x
    (e, f), (g, h) = y
    return ((a * e + b * g, a * f + b * h), (c * e + d * g, c * f + d * h))

def fib_matrix(n):
    """F(n) from [[1, 1], [1, 0]]^n by repeated squaring; also the multiplications used."""
    if n < 0:
        raise ValueError("n must be non-negative")
    result, power, mults = ((1, 0), (0, 1)), ((1, 1), (1, 0)), 0
    while n:
        if n & 1:
            result, mults = mat_mul(result, power), mults + 1
        n >>= 1
        if n:
            power, mults = mat_mul(power, power), mults + 1
    return result[0][1], mults

def binet_float(n):
    """Binet's formula evaluated in floating point and rounded to an integer."""
    root5 = math.sqrt(5)
    phi, psi = (1 + root5) / 2, (1 - root5) / 2
    return round((phi ** n - psi ** n) / root5)

def first_binet_failure(limit):
    """Smallest n < limit where the rounded float Binet value is wrong, or None."""
    for n, exact in enumerate(fib_list(limit)):
        if binet_float(n) != exact:
            return n
    return None

def cassini_holds(count):
    """Check F(n+1)F(n-1) - F(n)^2 == (-1)^n for 1 <= n < count."""
    f = fib_list(count + 1)
    return all(f[n + 1] * f[n - 1] - f[n] ** 2 == (-1) ** n
               for n in range(1, count))

def main():
    f = fib_list(300)
    print("F(0..12) from the recurrence:", f[:13])
    gf = series_divide([0, 1], [1, -1, -1], 300)
    print("Coefficients of x/(1 - x - x^2) agree for n < 300:", gf == f)
    same = all(fib_matrix(n)[0] == f[n] for n in range(300))
    print("Matrix powers agree for n < 300:", same)
    print("Cassini F(n+1)F(n-1) - F(n)^2 = (-1)^n for 1 <= n < 300:",
          cassini_holds(300))
    value, mults = fib_matrix(1000)
    print(f"F(1000) has {len(str(value))} digits; found with {mults} "
          "matrix products")
    print(f"(n log10(phi) predicts {1000 * math.log10((1 + 5 ** 0.5) / 2):.1f}"
          " digits)")
    n = first_binet_failure(200)
    print(f"Rounded float Binet first fails at n = {n}:")
    print(f"  exact F({n}) = {f[n]}")
    print(f"  float Binet  = {binet_float(n)}")
    print(f"  F({n}) has {len(str(f[n]))} digits. A float carries about 16, and")
    print("  the relative rounding error of phi grows about n-fold in phi^n.")
    print()
    print("Epistemic status: the agreements for n < 300 are exact integer")
    print("computations, i.e. exhaustive checks of finitely many cases; the")
    print("proofs for all n are in the lesson (and in Lean). The Binet failure")
    print("is a fact about 64-bit floating point, not about the formula,")
    print("which is exact in real arithmetic.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The second experiment counts balanced bracket strings by brute force and compares the counts with Segner's recurrence, the closed form, and the coefficients of $C(x)$ obtained by iterating $C \leftarrow 1 + x\,C^2$ on truncated series. Watch the iteration: each round fixes at least one more coefficient. This is convergence of formal power series in the " $x$ -adic" sense — two series are close when they agree in many leading coefficients — with no analysis at all. Finally it measures $C_n$ against $4^n/(\sqrt\pi\, n^{3/2})$ .

Catalan numbers four ways, and their growthPythonExhaustive finite checkExact computationNumerical approximationComputationally tested

"""Catalan numbers: brute force, a recurrence, a generating function, a formula.

We count balanced strings of n pairs of brackets by checking all 4^n strings
of length 2n (feasible for n <= 8), and compare with Segner's recurrence
C(n+1) = sum C(i) C(n-i), with the closed form binom(2n, n)/(n + 1), and with
the generating function C(x), which satisfies C(x) = 1 + x C(x)^2. We find
the coefficients of C(x) by iterating C <- 1 + x C^2 on truncated power
series: each round fixes at least one more coefficient, which is exactly how
formal power series "converge" with no analysis at all. Finally we compare
C(n) with the asymptotic formula 4^n / (sqrt(pi) n^(3/2)).
"""

import itertools
import math

def is_balanced(s):
    """True if the string of '(' and ')' is a balanced bracket sequence."""
    depth = 0
    for ch in s:
        depth += 1 if ch == "(" else -1
        if depth < 0:
            return False
    return depth == 0

def brute_force_count(n):
    """Number of balanced strings with n pairs, by checking all 4^n strings."""
    return sum(is_balanced(s) for s in itertools.product("()", repeat=2 * n))

def segner(count):
    """C(0), ..., C(count - 1) from C(0) = 1 and C(n+1) = sum C(i) C(n - i)."""
    c = [1]
    while len(c) < count:
        n = len(c) - 1
        c.append(sum(c[i] * c[n - i] for i in range(n + 1)))
    return c[:count]

def closed_form(n):
    """binom(2n, n) / (n + 1), which is always an integer."""
    q, r = divmod(math.comb(2 * n, n), n + 1)
    if r:
        raise ArithmeticError("binom(2n, n) should be divisible by n + 1")
    return q

def series_fixed_point(count, rounds):
    """Iterate C <- 1 + x*C^2, keeping the first `count` coefficients."""
    c = [0] * count
    for _ in range(rounds):
        square = [sum(c[i] * c[k - i] for i in range(k + 1))
                  for k in range(count)]
        c = [1] + square[: count - 1]
    return c

def asymptotic_ratio(n):
    """C(n) divided by 4^n / (sqrt(pi) n^(3/2)); computed with logarithms."""
    log_c = math.lgamma(2 * n + 1) - 2 * math.lgamma(n + 1) - math.log(n + 1)
    log_a = n * math.log(4) - 0.5 * math.log(math.pi) - 1.5 * math.log(n)
    return math.exp(log_c - log_a)

def main():
    rec = segner(16)
    print(" n  brute force  Segner  binom(2n,n)/(n+1)")
    for n in range(9):
        print(f"{n:2d}  {brute_force_count(n):11d}  {rec[n]:6d}  "
              f"{closed_form(n):17d}")
    ok = all(rec[n] == closed_form(n) for n in range(16))
    print("Segner = closed form for n < 16:", ok)
    for rounds in (3, 6, 16):
        c = series_fixed_point(16, rounds)
        agree = sum(1 for a, b in zip(c, rec) if a == b)
        print(f"{rounds:2d} rounds of C <- 1 + x C^2: {c[:7]}, "
              f"{agree}/16 correct")
    print("C(n) / (4^n / (sqrt(pi) n^1.5)):")
    for n in (10, 100, 1000):
        print(f"  n = {n:4d}: {asymptotic_ratio(n):.5f}")
    print("(the ratio is close to 1 - 9/(8n), so it tends to 1)")
    print()
    print("Epistemic status: the table is an exhaustive check of all strings")
    print("for n <= 8 plus exact integer arithmetic for n < 16; it proves")
    print("nothing about larger n (the reflection proof in the lesson does).")
    print("The ratios are floating-point evidence for the asymptotic formula,")
    print("which is proved with Stirling's formula.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Explore

Explore: ratios and growth rates

The ratio $r_n = F_{n+2}/F_{n+1}$ satisfies $r_{n+1} = 1 + 1/r_n$ — divide the recurrence by $F_{n+2}$ . So the ratios are the orbit of the map $x \mapsto 1 + 1/x$ starting from $r_0 = 1$ : $1, 2, 1.5, 1.667, 1.6, \dots$ The cobweb diagram shows them spiralling into the fixed point $\varphi$ , where $x = 1 + 1/x$ , i.e. $x^2 = x + 1$ . The spiral alternates sides because the derivative there, $-1/\varphi^2 \approx -0.38$ , is negative; its size is $|\psi/\varphi|$ , which is exactly the factor by which the error $r_n - \varphi$ shrinks per step according to Binet's formula.

Fibonacci ratios: iterating x ↦ 1 + 1/x

Start at x₀ = 1. The fixed point is the golden ratio φ ≈ 1.618.

The map f

f(x) =

Iterates xₖ against k

y = f(x)
y = x
cobweb path

Starting value x₀x₀ = 1Iterationsk = 20

Last iterates: x₁₈ = 1.61803, x₁₉ = 1.61803, x₂₀ = 1.61803

The orbit appears to settle at a fixed point x* ≈ 1.61803.

Fixed points in view (numerical): x* = 1.618 (attracting: |f′(x*)| < 1)

Based on 3,000 iterations in floating-point arithmetic: numerical evidence, not proof.

Big-O hides constants, but constants matter for small inputs. Below, $c\,n\log_2 n$ is compared with $n^2$ and $2^n$ . With $c = 4$ the curves $4n\log_2 n$ and $n^2$ cross (for $n \ge 2$ ) at $n = 16$ ; increase $c$ and watch the crossover move right — yet $n^2$ always wins eventually, because $n\log n = o(n^2)$ . The exponential leaves the picture almost at once.

Constants versus growth rates

Move the sliders and trace along the curves to read off values.

c · n log₂ n
n²
2ⁿ

cc = 4

Trace along xx = 1

c · n log₂ n: y = 0
n²: y = 1
2ⁿ: y = 2

Exercises

1. Recurrences and generating functions

Warm-upHuman

In how many ways can a $1 \times 9$ strip be tiled by $1 \times 1$ squares and $1 \times 2$ dominoes?

2. Recurrences and generating functions

Warm-upHuman

Find the characteristic roots of the recurrence $a_{n+2} = a_{n+1} + 6a_n$ . Enter them as a set, e.g. 4, -1.

3. Recurrences and generating functions

CoreHuman

The sequence $(a_n)$ satisfies $a_{n+2} = a_{n+1} + 6a_n$ with $a_0 = 2$ and $a_1 = 1$ . Find a closed formula for $a_n$ and use it to compute $a_5$ .

4. Recurrences and generating functions

CoreHuman

Which formula describes all solutions of $a_{n+2} = 6a_{n+1} - 9a_n$ (with $A$ , $B$ arbitrary constants)?

Choose one

a_n = (A + Bn)\,3^n

a_n = A\,3^n + B\,3^n

a_n = A\,3^n + B(-3)^n

a_n = (A + Bn^2)\,3^n

5. Recurrences and generating functions

CoreHuman

The power series $\sum_{n \ge 0} n!\,x^n$ converges only at $x = 0$ . Which statement about it, as an element of the ring $\Q[[x]]$ of formal power series, is true?

Choose one

It has a multiplicative inverse in

\Q[[x]]

.It is not a valid element of

\Q[[x]]

, because it diverges.It can be added to other series but not multiplied, because products would diverge.It is invertible only if we restrict to

x = 0

6. Recurrences and generating functions

CoreHuman

Which of these statements are true? (Choose all that apply.)

Choose all that apply

n^2 = O(n^3)

n^3 = O(n^2)

2^{n+1} = O(2^n)

4^n = O(2^n)

\log_2 n = \Theta(\ln n)

n \log n = \Omega(n)

7. Recurrences and generating functions

CoreHuman

In the proof of Lemma 2 (two solutions of $a_{n+2} = p\,a_{n+1} + q\,a_n$ with the same $a_0$ and $a_1$ agree everywhere), the induction proves the statement " $a_n = b_n$ and $a_{n+1} = b_{n+1}$ " rather than just " $a_n = b_n$ ". Why?

Choose one

To deduce

a_{n+2} = b_{n+2}

from the recurrence we need equality at two consecutive indices, so the inductive hypothesis must carry both.Because

p

q

might be zero.Because ordinary induction is not valid for sequences.Because the characteristic roots might be repeated.

8. Recurrences and generating functions

CoreFormal

Using the lesson's definition IsSol p q a (meaning ∀ n, a (n + 2) = p * a (n + 1) + q * a n), which Lean statement correctly formalises: every real sequence satisfying $a_{n+2} = a_{n+1} + a_n$ with $a_0 = 0$ and $a_1 = 1$ is the Fibonacci sequence?

Choose one

∀ a : ℕ → ℝ, IsSol 1 1 a → a 0 = 0 → a 1 = 1 → ∀ n, a n = Nat.fib n∀ a : ℕ → ℝ, IsSol 1 1 a → ∀ n, a n = Nat.fib n∃ a : ℕ → ℝ, IsSol 1 1 a ∧ a 0 = 0 ∧ a 1 = 1∀ a : ℕ → ℝ, a 0 = 0 → a 1 = 1 → ∀ n, a n = Nat.fib n

9. Recurrences and generating functions

CoreHuman

In how many ways can the product $x_1 x_2 x_3 x_4 x_5 x_6$ be fully bracketed, keeping the factors in order? (For three factors there are two: $(x_1x_2)x_3$ and $x_1(x_2x_3)$ .)

10. Recurrences and generating functions

StretchComputational

Write series_inverse(a, N) that returns the first N coefficients of $1/A(x)$ , where a is the list of coefficients of a power series $A(x)$ with a[0] == 1 (missing coefficients count as $0$ ). Use the recursion from the Proposition on inverses: $b_0 = 1$ and $b_n = -\sum_{i=1}^{n} a_i b_{n-i}$ . Then check that $1/(1 - x - x^2)$ gives the Fibonacci numbers $F_{n+1}$ .

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"A formal power series has to converge to mean anything." In $K[[x]]$ a series is its sequence of coefficients, and sums and products are computed coefficient by coefficient with finite sums. $\sum n!\,x^n$ converges only at $x = 0$ , yet it is a perfectly good element of $\Q[[x]]$ with an inverse (proved in Lean above). Convergence matters only when you want to substitute a number for $x$ , or to use analysis to read off asymptotics.

Misconception

"Big-O is the exact running time" or "big-O is a lower bound". $f = O(g)$ is an upper bound up to a constant factor, valid for large $n$ . Mergesort is $O(n^2)$ as well as $O(n\log n)$ — both are true, the second is sharper. For "exactly this order" use $\Theta$ , for a lower bound $\Omega$ . And because constants are hidden, an $O(n\log n)$ algorithm can be slower than an $O(n^2)$ one for all inputs you will ever meet.

Misconception

"The first few terms reveal the formula." Place $n$ points on a circle and join every pair by a chord; for points in general position the regions number $1, 2, 4, 8, 16$ for $n = 1, \dots, 5$ — and then $31$ , not $32$ . (The true count is $\binom{n}{4} + \binom{n}{2} + 1$ .) A guessed formula must be proved, for instance by checking that it satisfies the recurrence and the initial values.

Misconception

"Any recurrence can be solved by the characteristic polynomial." The method needs a recurrence that is linear with constant coefficients and a fixed look-back. It does not apply to $x_{n+1} = r x_n(1 - x_n)$ , to $a_n = n\,a_{n-1}$ , or directly to $T(n) = 2T(n/2) + n$ .

Misconception

"One initial value is enough." A recurrence of order $k$ needs $k$ initial values: $a_{n+2} = a_{n+1} + a_n$ with $a_0 = 2$ , $a_1 = 1$ gives the Lucas numbers $2, 1, 3, 4, 7, 11, \dots$ , not the Fibonacci numbers. The solution space has dimension $k$ .

ViewpointsH

Many ways of seeing

Algebra— The shift operator, and recurrences as linear algebra

Let $E$ be the shift on sequences, $(Ea)_n = a_{n+1}$ . The recurrence $a_{n+k} = c_1 a_{n+k-1} + \cdots + c_k a_n$ says $\chi(E)\,a = 0$ : solutions are the kernel of the linear operator $\chi(E)$ . Since $\chi(E)$ factors as $\prod (E - r_i)^{m_i}$ and the factors commute, the kernel splits into the kernels of $(E - r_i)^{m_i}$ , each spanned by $n^j r_i^n$ for $j < m_i$ . This is the same algebra as solving $p(D)y = 0$ for the differentiation operator $D$ , where $e^{rt}$ replaces $r^n$ and $t^j e^{rt}$ replaces $n^j r^n$ — compare ordinary differential equations.

In matrix form, $\begin{pmatrix} F_{n+1} \\ F_n \end{pmatrix} = M^n \begin{pmatrix} 1 \\ 0 \end{pmatrix}$ with the companion matrix $M = \begin{pmatrix} 1 & 1 \\ 1 & 0 \end{pmatrix}$ , and indeed $M^n = \begin{pmatrix} F_{n+1} & F_n \\ F_n & F_{n-1} \end{pmatrix}$ . The characteristic roots are the eigenvalues of $M$ , and diagonalising $M$ is Binet's formula. Taking determinants, $\det M^n = (-1)^n$ gives Cassini's identity $F_{n+1}F_{n-1} - F_n^2 = (-1)^n$ . A repeated root corresponds to a companion matrix that cannot be diagonalised, and $n r^n$ comes from its Jordan block. See linear algebra.

Analysis— Singularities decide growth

Substitute a complex number for $x$ , and a generating function with positive radius of convergence $R$ becomes an analytic function. By the Cauchy–Hadamard formula, $\limsup |a_n|^{1/n} = 1/R$ : the exponential growth rate of the coefficients is the reciprocal of the distance to the nearest singularity. For $F(x) = x/(1 - x - x^2)$ the singularities are the roots $1/\varphi \approx 0.618$ and $-\varphi$ of $1 - x - x^2$ , so $F_n$ grows like $\varphi^n$ . For the Catalan function $(1 - \sqrt{1 - 4x})/(2x)$ the singularity is at $x = \tfrac14$ , so the growth rate is $4^n$ ; its type — a square root — produces the factor $n^{-3/2}$ . Turning the shape of a singularity into precise asymptotics is the subject of analytic combinatorics (Flajolet and Sedgewick), whose transfer theorems (Flajolet and Odlyzko, 1990) make this rigorous. See complex analysis.

Number theory— The arithmetic of Fibonacci numbers

Fibonacci numbers have striking divisibility: $\gcd(F_m, F_n) = F_{\gcd(m, n)}$ (Lucas, 1876), so $F_m$ divides $F_n$ whenever $m$ divides $n$ , and $F_n$ can be prime only if $n = 4$ or $n$ is prime ( $F_{19} = 4181 = 37 \cdot 113$ shows the converse fails). Whether there are infinitely many Fibonacci primes is an open problem. Reduced modulo any $m$ , the sequence is periodic (the Pisano period): there are only $m^2$ possible consecutive pairs, so some pair repeats, and since the recurrence can be run backwards ( $F_n = F_{n+2} - F_{n+1}$ ) the sequence is purely periodic. Modulo $10$ the period is $60$ , which is why last digits of Fibonacci numbers repeat every $60$ terms. A related recurrence powers the Lucas–Lehmer test: for an odd prime $p$ , the Mersenne number $2^p - 1$ is prime if and only if $s_{p-2} \equiv 0 \pmod{2^p - 1}$ , where $s_0 = 4$ and $s_{k+1} = s_k^2 - 2$ . It is how the largest known primes are found.

Combinatorics— The symbolic method

Generating functions translate constructions into operations: disjoint union of classes ↦ sum, pairs ↦ product, sequences ↦ $1/(1 - A)$ . So "a rhythm is a sequence of beats of size $1$ or $2$ " translates at once into $1/(1 - x - x^2)$ , and "a binary tree is empty or a root with a left and a right subtree" into $B = 1 + xB^2$ — the Catalan equation, which explains why binary trees are counted by $C_n$ . The same dictionary, with $\sum a_n x^n/n!$ (exponential generating functions), handles labelled objects such as permutations and set partitions. A nice consequence in the other direction is Zeckendorf's theorem: every positive integer is uniquely a sum of non-consecutive Fibonacci numbers $F_k$ with $k \ge 2$ (for example $100 = 89 + 8 + 3$ ). See enumerative combinatorics.

Probability— Waiting for two heads

Toss a fair coin until two heads appear in a row. Let $E$ be the expected number of tosses from the start, and $E_H$ the expected number still needed just after a head. Conditioning on the next toss gives the linear system $E = 1 + \tfrac12 E_H + \tfrac12 E$ and $E_H = 1 + \tfrac12 \cdot 0 + \tfrac12 E$ , so $E = 6$ . The probability of no two consecutive heads in $n$ tosses is $F_{n+2}/2^n$ , because such strings are counted by the rhythm recurrence — so it decays like $(\varphi/2)^n$ . The probability generating function $G(s) = \mathbb{E}[s^T] = \sum P(T = n)s^n$ of the waiting time $T$ satisfies a recurrence-derived equation too, and $G'(1) = \mathbb{E}[T]$ . Linear recurrences for probabilities are the backbone of Markov chains.

Computation— Three algorithms for Fₙ

Computing $F_n$ by the naive recursion fib(n) = fib(n-1) + fib(n-2) makes $2F_{n+1} - 1$ calls — exponentially many, $\Theta(\varphi^n)$ , because the same subproblems are solved again and again. Storing the values (memoisation, the idea behind dynamic programming) brings this down to $n$ additions. The matrix identity, with $M^{2m} = (M^m)^2$ , needs only $O(\log n)$ multiplications. But $F_n$ has about $0.209\,n$ decimal digits, so for large $n$ the cost is dominated by multiplying huge integers, not by the number of operations. In the other direction, Gabriel Lamé (1844) proved that if Euclid's algorithm on $a > b$ takes $k$ division steps then $b \ge F_{k+1}$ — so the number of steps is at most about five times the number of decimal digits of $b$ , with consecutive Fibonacci numbers as the worst case. It is one of the first analyses of an algorithm's running time. See algorithm design.

History & global context

History and global context

Indian prosody. Pingala's Chandaḥśāstra (its date is uncertain, perhaps the last centuries BCE) studied the enumeration of poetic metres. The rule that the number of metres of total length $n$ , built from short and long syllables, is the sum of the two previous counts is stated explicitly by Virahāṅka (between 600 and 800 CE), and again by Gopāla (before 1135) and Hemacandra (c. 1150).
Leonardo of Pisa. In Liber Abaci (1202) Leonardo — later called Fibonacci — posed the rabbit problem whose answers are $1, 2, 3, 5, 8, \dots$ . Johannes Kepler remarked (1611) that the ratios of consecutive terms approach the golden ratio. The name "Fibonacci numbers" is due to Édouard Lucas in the 1870s, who also proved their divisibility properties.
Generating functions. Abraham de Moivre introduced generating functions to solve linear recurrences ("recurrent series") in Miscellanea Analytica (1730), obtaining the closed form for the Fibonacci numbers; Daniel Bernoulli found it independently (1728), and Jacques Binet rediscovered it in 1843, giving it his name. Leonhard Euler used generating functions for partitions (Introductio in analysin infinitorum, 1748), and Pierre-Simon Laplace made them a central tool of probability (Théorie analytique des probabilités, 1812).
Catalan numbers. The Mongolian astronomer and mathematician Minggatu (Ming Antu) found them in the 1730s in power-series expansions of trigonometric functions (published posthumously in 1839). Euler counted triangulations of polygons in a letter to Christian Goldbach (1751), Johann Andreas von Segner gave the recurrence (1758), and Eugène Catalan studied bracketings (1838). The reflection argument is traditionally credited to Désiré André (1887), whose own proof of the closely related ballot theorem was in fact a slightly different bijection.
Asymptotic notation. Paul Bachmann introduced $O$ (1894) and Edmund Landau popularised it and added $o$ (1909). Donald Knuth proposed the now-standard meanings of $\Omega$ and $\Theta$ for the analysis of algorithms (1976); G. H. Hardy and J. E. Littlewood had earlier used $\Omega$ in a different sense (1914). The master theorem is due to Jon Bentley, Dorothea Haken and James Saxe (1980).

Counting by remembering

Unroll, guess, verify — and the sequence as one object

Definitions

Worked examples and non-examples

Linear recurrences: the characteristic-root theorem

Generating functions

Catalan numbers

How fast does it grow?

Recurrences in Lean and Mathlib

Experiments: four routes to Fibonacci, four routes to Catalan

Explore: ratios and growth rates

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading