divide_and_conquer_equal_roots_recurrence
theoremverified
For any real branching factor a, base value d and step cost c, the recurrence T(k+1) = a*T(k) + c*a^(k+1) has exact solution T(k) = d*a^k + c*k*a^k.
Statement
theorem divide_and_conquer_equal_roots_recurrence
(T : ℕ → ℝ) (a c d : ℝ)
(h0 : T 0 = d)
(hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * a ^ (k + 1)) :
∀ k : ℕ, T k = d * a ^ k + c * (k : ℝ) * a ^ k- Verified
- 06 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Used by 1
- divide_and_conquer_mergesort_recurrenceThe mergesort recurrence T(k+1) = 2*T(k) + c*2^(k+1) with base cost T(0) = d has exact solution T(k) = d*2^k + c*k*2^k.
Lean source view module on GitHub
/-- Closed-form solution to the divide-and-conquer recurrence with equal roots T(k+1) = a * T(k) + c * a^(k+1). -/ theorem divide_and_conquer_equal_roots_recurrence (T : ℕ → ℝ) (a c d : ℝ) (h0 : T 0 = d) (hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * a ^ (k + 1)) : ∀ k : ℕ, T k = d * a ^ k + c * (k : ℝ) * a ^ k := by intro k induction' k with k ih · simp [h0] · rw [hrec k, ih] push_cast ring