AFTD Auto-Formalizing Theoretical Domains

master_theorem_polynomial_case_three

theoremverified

Let 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 problem size n = b^k, namely T(k+1) = a·T(k) + c·b^{d(k+1)}. If b^d < a (the branching term dominates), then for every k ≥ 1 the value T(k) is Θ(n^{log_b a}) with n = b^k, in the explicit two-sided form (c·b^d/a)·a^k ≤ T(k) ≤ (T(0) + c·b^d/(a − b^d))·a^k.

Statement

theorem master_theorem_polynomial_case_three (T : ℕ → ℝ) (a b c : ℝ) (d : ℕ)
    (hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * b ^ (d * (k + 1)))
    (hT0 : 0 ≤ T 0) (ha : 0 ≤ a) (hb : 1 < b) (hc : 0 ≤ c) (hgt : b ^ d < a) :
    ∀ k : ℕ, 1 ≤ k →
      c * b ^ d / a * a ^ k ≤ T k ∧ T k ≤ (T 0 + c * b ^ d / (a - b ^ d)) * a ^ k
Source
CLRS, Introduction to Algorithms, Thm 4.1 (master theorem), specialised to f(n) = c·n^d with n = b^k; cf. Kleinberg & Tardos, Chapter 5
Verified
10 Sep 2026
Axioms
Classical.choiceQuot.soundpropext
Built on 2

Read back from the Lean

For every function T : ℕ → ℝ, every real numbers a, b, c, and every natural number d, suppose all of the following hypotheses hold: 1. For every natural number k, T(k+1) = a·T(k) + c·b^(d·(k+1)). 2. 0 ≤ T(0). 3. 0 ≤ a. 4. 1 < b. 5. 0 ≤ c. 6. b^d < a. Then for every natural number k with 1 ≤ k, both ((c·b^d)/a)·a^k ≤ T(k) and T(k) ≤ (T(0) + (c·b^d)/(a − b^d))·a^k. All arithmetic is in ℝ; powers are natural-exponent powers. The recurrence and all listed inequalities are hypotheses of the implication, and the conclusion is asserted only for k ≥ 1, not for 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

theorem master_theorem_polynomial_case_three (T : ℕ → ℝ) (a b c : ℝ) (d : ℕ)
    (hrec : ∀ k : ℕ, T (k + 1) = a * T k + c * b ^ (d * (k + 1)))
    (hT0 : 0 ≤ T 0) (ha : 0 ≤ a) (hb : 1 < b) (hc : 0 ≤ c) (hgt : b ^ d < a) :
    ∀ k : ℕ, 1 ≤ k →
      c * b ^ d / a * a ^ k ≤ T k ∧ T k ≤ (T 0 + c * b ^ d / (a - b ^ d)) * a ^ k := by
  have hb0 : 0 < b := lt_trans zero_lt_one hb
  have hrpos : 0 < b ^ d := pow_pos hb0 d
  have hrnonneg : 0 ≤ b ^ d := le_of_lt hrpos
  have hapos : 0 < a := lt_trans hrpos hgt
  have hden : 0 < a - b ^ d := sub_pos.mpr hgt
  have hane : a ≠ b ^ d := ne_of_gt hgt
  have hsol : ∀ k : ℕ, T k = T 0 * a ^ k + c * b ^ d * ((a ^ k - (b ^ d) ^ k) / (a - b ^ d)) := by
    apply divide_and_conquer_unequal_roots_recurrence T a (b ^ d) c (T 0) hane rfl
    intro k
    rw [hrec k, pow_mul]
  intro k hk
  constructor
  · rw [hsol k]
    have hT0term : 0 ≤ T 0 * a ^ k := mul_nonneg hT0 (pow_nonneg ha k)
    have hpow : (b ^ d) ^ (k - 1) ≤ a ^ (k - 1) := pow_le_pow_left₀ hrnonneg (le_of_lt hgt) (k - 1)
    have hk_eq : k - 1 + 1 = k := Nat.sub_add_cancel hk
    have hak : a ^ k = a ^ (k - 1) * a := by
      conv_lhs => rw [← hk_eq]
      rw [pow_succ]
    have hrk : (b ^ d) ^ k = (b ^ d) ^ (k - 1) * (b ^ d) := by
      conv_lhs => rw [← hk_eq]
      rw [pow_succ]
    have hkey : (b ^ d) ^ k * a ≤ a ^ k * (b ^ d) := by
      rw [hak, hrk]
      nlinarith [mul_le_mul_of_nonneg_right hpow (mul_nonneg hrnonneg (le_of_lt hapos))]
    have hterm' : a ^ k / a ≤ (a ^ k - (b ^ d) ^ k) / (a - b ^ d) := by
      rw [div_le_div_iff₀ hapos hden]
      nlinarith [hkey]
    have hterm : c * b ^ d / a * a ^ k ≤ c * b ^ d * ((a ^ k - (b ^ d) ^ k) / (a - b ^ d)) := by
      have heq : c * b ^ d / a * a ^ k = c * b ^ d * (a ^ k / a) := by
        rw [div_eq_mul_inv, div_eq_mul_inv]; ring
      rw [heq]
      exact mul_le_mul_of_nonneg_left hterm' (mul_nonneg hc hrnonneg)
    exact le_trans hterm (le_add_of_nonneg_left hT0term)
  · have hU : (T 0 + c * b ^ d / (a - b ^ d)) * a ^ k - T k = c * b ^ d * (b ^ d) ^ k / (a - b ^ d) := by
      rw [hsol k]
      field_simp
      ring
    have hUnn : 0 ≤ c * b ^ d * (b ^ d) ^ k / (a - b ^ d) :=
      div_nonneg (mul_nonneg (mul_nonneg hc hrnonneg) (pow_nonneg hrnonneg k)) (le_of_lt hden)
    linarith [hU, hUnn]
Discuss this resultChallenge it