divide_and_conquer_unequal_roots_recurrence

theoremverified

For real branching factor a and cost ratio r with a != r, base value d and cost scale c, the recurrence T(k+1) = a*T(k) + c*r^(k+1) with T(0) = d has exact solution T(k) = d*a^k + c*r*(a^k - r^k)/(a - r).

Statement

theorem divide_and_conquer_unequal_roots_recurrence
    (T : ℕ → ℝ) (a r c d : ℝ) (har : a ≠ r)
    (h0 : T 0 = d)
    (hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * r ^ (k + 1)) :
    ∀ k : ℕ, T k = d * a ^ k + c * r * ((a ^ k - r ^ k) / (a - r))

Source

Cormen, Leiserson, Rivest & Stein, Introduction to Algorithms, 3rd ed., Section 4.6

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

Let $T : \mathbb{N} \to \mathbb{R}$ be a sequence of real numbers and let $a, r, c, d \in \mathbb{R}$ be real numbers. Assume $a \neq r$, $T(0) = d$, and for all $k \in \mathbb{N}$, $T(k + 1) = a T(k) + c r^{k + 1}$. Then for all $k \in \mathbb{N}$, $$T(k) = d a^k + c r \left(\frac{a^k - r^k}{a - r}\right).$$

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 exact solution of the divide-and-conquer recurrence with unequal roots (a ≠ r), corresponding to Master theorem cases 1 and 3. -/
theorem divide_and_conquer_unequal_roots_recurrence
    (T : ℕ → ℝ) (a r c d : ℝ) (har : a ≠ r)
    (h0 : T 0 = d)
    (hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * r ^ (k + 1)) :
    ∀ k : ℕ, T k = d * a ^ k + c * r * ((a ^ k - r ^ k) / (a - r)) := by
  intro k
  induction k with
  | zero => simp [h0]
  | succ k ih =>
    rw [hrec, ih]
    have h_sub : a - r ≠ 0 := sub_ne_zero.mpr har
    rw [pow_succ a k, pow_succ r k]
    field_simp
    ring

Discuss this result Challenge it