divide_and_conquer_recursion_tree

theoremverified

For any branching factor a and cost function g, the divide-and-conquer recurrence T(k+1) = a*T(k) + g(k+1) has exact solution T(k) = a^k * T(0) + sum_{j=1}^k a^(k-j) * g(j).

Statement

theorem divide_and_conquer_recursion_tree
    (T : ℕ → ℝ) (g : ℕ → ℝ) (a : ℝ)
    (hrec : ∀ k : ℕ, T (k + 1) = a * T k + g (k + 1)) :
    ∀ k : ℕ, T k = a ^ k * T 0 + Finset.sum (Finset.Icc 1 k) (fun j => a ^ (k - j) * g j)

Source

Cormen, Leiserson, Rivest & Stein, Introduction to Algorithms, 3rd ed., Section 4.6 (Lemma 4.1)

Verified

07 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Used by 2

master_theorem_polynomial_case_threeLet a ≥ 0, b > 1 and c ≥ 0 be real numbers, d a natural number, and T : ℕ → ℝ a sequence with T(0) ≥ 0 satisfying the master recurrence at…
master_theorem_polynomial_case_oneLet a ≥ 0, b > 1 and c ≥ 0 be real numbers, d a natural number, and T : ℕ → ℝ a sequence with T(0) ≥ 0 satisfying the master recurrence at…

Read back from the Lean

Given functions $T, g : \mathbb{N} \to \mathbb{R}$ and a real number $a$, if for every $k \in \mathbb{N}$, $T(k + 1) = a \cdot T(k) + g(k + 1)$, then for every $k \in \mathbb{N}$, $T(k) = a^k \cdot T(0) + \sum_{j \in [1, k]} a^{k - j} \cdot g(j)$, where the sum is indexed by the finset of natural numbers $j \in [1, k]$ (and equals $0$ when $k = 0$).

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- The general recursion tree summation formula for divide-and-conquer recurrences T(k+1) = a*T(k) + g(k+1). -/
theorem divide_and_conquer_recursion_tree
    (T : ℕ → ℝ) (g : ℕ → ℝ) (a : ℝ)
    (hrec : ∀ k : ℕ, T (k + 1) = a * T k + g (k + 1)) :
    ∀ k : ℕ, T k = a ^ k * T 0 + Finset.sum (Finset.Icc 1 k) (fun j => a ^ (k - j) * g j) := by
  intro k
  induction k with
  | zero => simp
  | succ k ih =>
    rw [hrec k, ih]
    rw [Finset.sum_Icc_succ_top (by omega)]
    have hsum : a * (∑ j ∈ Finset.Icc 1 k, a ^ (k - j) * g j) =
        ∑ j ∈ Finset.Icc 1 k, a ^ (k + 1 - j) * g j := by
      rw [Finset.mul_sum]
      apply Finset.sum_congr rfl
      intro j hj
      have hj' : j ≤ k := (Finset.mem_Icc.mp hj).2
      have : a * (a ^ (k - j) * g j) = (a * a ^ (k - j)) * g j := by ring
      rw [this, ← pow_succ']
      congr 2
      omega
    simp only [Nat.sub_self, pow_zero, one_mul]
    have : a * (a ^ k * T 0) = a ^ (k + 1) * T 0 := by
      rw [← mul_assoc, ← pow_succ']
    linarith

Discuss this result Challenge it