CLRS-Lean
Chapters 1–35 · CLRS Fourth Edition
Chapter 4. Divide-and-Conquer
4.5. The Master Method for Solving Recurrences

Imports

import CLRSLean.Chapter_03.Section_03_1_Asymptotic_Notation
import Mathlib.Tactic

open Finsetopen scoped BigOperators

4.5. The Master Method for Solving Recurrences

This file proves the exact-power algebraic core of the Chapter 4 Master Theorem. For recurrences on exact powers, T(b^(i+1)) = a * T(b^i) + f(b^(i+1)), the normalized quantity T(b^i) / a^i unfolds into the initial value plus a finite sum of normalized forcing terms. The three Master-style exact-power criteria below then turn bounded, constant, or tail-dominated normalized forcing into the expected asymptotic conclusions.

Main result:

Theorem CLRS.Chapter04.h_formula: the normalized exact-power recurrence expansion.
Theorem CLRS.Chapter04.master_case1_geometric: bounded normalized forcing, obtained from a geometric upper bound, gives T(b^i) = Θ(a^i).
Theorem CLRS.Chapter04.master_case2_constant_forcing: constant normalized forcing gives T(b^i) = Θ((i+1)a^i).
Theorem CLRS.Chapter04.master_case2_polylog_forcing: polynomial normalized forcing c·j^k ≤ forcing ≤ C·j^k (the f(n) = Θ(n^(log_b a)·log^k n) textbook case) gives T(b^i) = Θ((i+1)^(k+1)a^i).
Theorem CLRS.Chapter04.master_case3_tail_dominated: a conditional normalized tail-domination criterion.
Theorem CLRS.Chapter04.master_case3_of_eventual_regularity: eventual forcing regularity derives T(b^i) = Θ(f(b^i)), absorbing the finite prefix into an explicitly constructed constant.
Theorem CLRS.Chapter04.normalized_tail_upper_of_eventual_regularity: supplies the normalized upper-bound premise of the legacy all-input wrappers.

Status: proved for these exact-power criteria, including case-3 regularity with nonnegative costs and positive forcing at the regularity threshold. The all-input transfer in Section 4.6 retains explicit monotonicity and adjacent-scale bounds; these hypotheses are not derived here.

namespace CLRSnamespace Chapter04

Exact-power recurrences

Exact-power form of the CLRS Master Theorem recurrence.

structure ExactPowerRecurrence (a b : ℕ) (f T : ℕ → ℝ) : Prop where
  step : ∀ i : ℕ, T (b ^ (i + 1)) = (a : ℝ) * T (b ^ i) + f (b ^ (i + 1))

The normalized value T(b^i) / a^i.

noncomputable def normalizedValue (a b : ℕ) (T : ℕ → ℝ) (i : ℕ) : ℝ :=
  T (b ^ i) / ((a : ℝ) ^ i)

The normalized forcing term contributed at the step from i to i+1.

noncomputable def normalizedForcing (a b : ℕ) (f : ℕ → ℝ) (i : ℕ) : ℝ :=
  f (b ^ (i + 1)) / ((a : ℝ) ^ (i + 1))

Public theorem

Unroll the exact-power recurrence after dividing by a^i.

This is the algebraic spine of the Master Theorem proof: the remaining CLRS case analysis is a question about bounding the finite sum on the right-hand side.


theorem h_formula (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (ha_ne_zero : (a : ℝ) ≠ 0)
    (i : ℕ) :
    T (b ^ i) / ((a : ℝ) ^ i) =
      T (b ^ 0) / ((a : ℝ) ^ 0) +
        (∑ k ∈ range i, f (b ^ (k + 1)) / ((a : ℝ) ^ (k + 1))) := by
  induction' i with i ih
  · simp
  · rw [show
        T (b ^ (i + 1)) / ((a : ℝ) ^ (i + 1)) =
          T (b ^ i) / ((a : ℝ) ^ i) +
            f (b ^ (i + 1)) / ((a : ℝ) ^ (i + 1)) by
        field_simp [ha_ne_zero, pow_succ]
        rw [h_rec.step i]
        ring]
    rw [ih]
    simp [sum_range_succ, add_assoc]

lemma normalizedValue_eq_base_add_sum (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (ha_ne_zero : (a : ℝ) ≠ 0)
    (i : ℕ) :
    normalizedValue a b T i =
      normalizedValue a b T 0 +
        (∑ k ∈ range i, normalizedForcing a b f k) := by
  simpa [normalizedValue, normalizedForcing] using
    h_formula a b f T h_rec ha_ne_zero i

private theorem isBigTheta_of_eventual_bounds {f g : ℕ → ℝ}
    (hO : ∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, ∀ n, n ≥ n₀ → |f n| ≤ C * |g n|)
    (hΩ : ∃ c : ℝ, 0 < c ∧ ∃ n₀ : ℕ, ∀ n, n ≥ n₀ → c * |g n| ≤ |f n|) :
    Chapter03.isBigTheta f g := by
  exact ⟨(Chapter03.isBigO_iff f g).2 hO, (Chapter03.isBigOmega_iff f g).2 hΩ⟩

If the normalized recurrence values are eventually within constant multiples of a nonnegative scale s, then the original exact-power recurrence is Θ(s(i)a^i).


theorem theta_of_normalized_by_scale (a b : ℕ) (T : ℕ → ℝ) (scale : ℕ → ℝ)
    (ha_pos : 0 < (a : ℝ))
    (hscale_nonneg : ∀ i, 0 ≤ scale i)
    (h_lower :
      ∃ c : ℝ, 0 < c ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ →
        c * scale i ≤ normalizedValue a b T i)
    (h_upper :
      ∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ →
        normalizedValue a b T i ≤ C * scale i) :
    Chapter03.isBigTheta
      (fun i : ℕ => T (b ^ i))
      (fun i : ℕ => scale i * ((a : ℝ) ^ i)) := by
  rcases h_lower with ⟨c, hc_pos, nL, hL⟩
  rcases h_upper with ⟨C, hC_pos, nU, hU⟩
  have ha_ne_zero : (a : ℝ) ≠ 0 := ne_of_gt ha_pos
  refine isBigTheta_of_eventual_bounds ?_ ?_
  · refine ⟨C, hC_pos, max nL nU, ?_⟩
    intro i hi
    have hiL : i ≥ nL := le_trans (Nat.le_max_left _ _) hi
    have hiU : i ≥ nU := le_trans (Nat.le_max_right _ _) hi
    have hscale_i := hscale_nonneg i
    have hnv_nonneg : 0 ≤ normalizedValue a b T i := by
      have hmul_nonneg : 0 ≤ c * scale i := mul_nonneg hc_pos.le hscale_i
      exact hmul_nonneg.trans (hL i hiL)
    have hT_eq :
        T (b ^ i) = ((a : ℝ) ^ i) * normalizedValue a b T i := by
      dsimp [normalizedValue]
      field_simp [pow_ne_zero i ha_ne_zero]
    have hT_abs :
        |T (b ^ i)| = ((a : ℝ) ^ i) * normalizedValue a b T i := by
      rw [hT_eq, abs_mul, abs_of_nonneg (pow_nonneg ha_pos.le i),
        abs_of_nonneg hnv_nonneg]
    have htarget_abs :
        |scale i * ((a : ℝ) ^ i)| = scale i * ((a : ℝ) ^ i) := by
      rw [abs_of_nonneg (mul_nonneg hscale_i (pow_nonneg ha_pos.le i))]
    calc
      |T (b ^ i)| = ((a : ℝ) ^ i) * normalizedValue a b T i := hT_abs
      _ ≤ ((a : ℝ) ^ i) * (C * scale i) := by
        gcongr
        exact hU i hiU
      _ = C * (scale i * ((a : ℝ) ^ i)) := by ring
      _ = C * |scale i * ((a : ℝ) ^ i)| := by rw [htarget_abs]
  · refine ⟨c, hc_pos, max nL nU, ?_⟩
    intro i hi
    have hiL : i ≥ nL := le_trans (Nat.le_max_left _ _) hi
    have hscale_i := hscale_nonneg i
    have hnv_nonneg : 0 ≤ normalizedValue a b T i := by
      have hmul_nonneg : 0 ≤ c * scale i := mul_nonneg hc_pos.le hscale_i
      exact hmul_nonneg.trans (hL i hiL)
    have hT_eq :
        T (b ^ i) = ((a : ℝ) ^ i) * normalizedValue a b T i := by
      dsimp [normalizedValue]
      field_simp [pow_ne_zero i ha_ne_zero]
    have hT_abs :
        |T (b ^ i)| = ((a : ℝ) ^ i) * normalizedValue a b T i := by
      rw [hT_eq, abs_mul, abs_of_nonneg (pow_nonneg ha_pos.le i),
        abs_of_nonneg hnv_nonneg]
    have htarget_abs :
        |scale i * ((a : ℝ) ^ i)| = scale i * ((a : ℝ) ^ i) := by
      rw [abs_of_nonneg (mul_nonneg hscale_i (pow_nonneg ha_pos.le i))]
    calc
      c * |scale i * ((a : ℝ) ^ i)| = c * (scale i * ((a : ℝ) ^ i)) := by
        rw [htarget_abs]
      _ = ((a : ℝ) ^ i) * (c * scale i) := by ring
      _ ≤ ((a : ℝ) ^ i) * normalizedValue a b T i := by
        gcongr
        exact hL i hiL
      _ = |T (b ^ i)| := by rw [hT_abs]

private lemma geometric_sum_le_tsum_bound {r : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1)
    (i : ℕ) :
    (∑ k ∈ range i, r ^ k) ≤ (1 - r)⁻¹ := by
  have hsumm : Summable fun k : ℕ => r ^ k := summable_geometric_of_lt_one hr_nonneg hr_lt_one
  calc
    (∑ k ∈ range i, r ^ k) ≤ ∑' k : ℕ, r ^ k :=
      hsumm.sum_le_tsum (range i) (fun k _ => pow_nonneg hr_nonneg k)
    _ = (1 - r)⁻¹ := tsum_geometric_of_lt_one hr_nonneg hr_lt_one

Master case 1, exact-power form: if the normalized forcing terms are bounded by a convergent geometric sequence, then T(b^i) = Θ(a^i).


theorem master_case1_geometric (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (ha_pos : 0 < (a : ℝ))
    (h_base_pos : 0 < normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    {r C : ℝ} (hr_nonneg : 0 ≤ r) (hr_lt_one : r < 1) (hC_pos : 0 < C)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C * r ^ k) :
    Chapter03.isBigTheta
      (fun i : ℕ => T (b ^ i))
      (fun i : ℕ => ((a : ℝ) ^ i)) := by
  have ha_ne_zero : (a : ℝ) ≠ 0 := ne_of_gt ha_pos
  have hsum_bound :
      ∃ B : ℝ, 0 ≤ B ∧
        ∀ i, (∑ k ∈ range i, normalizedForcing a b f k) ≤ B := by
    refine ⟨C * (1 - r)⁻¹, mul_nonneg hC_pos.le (inv_nonneg.mpr (sub_nonneg.mpr hr_lt_one.le)), ?_⟩
    intro i
    calc
      (∑ k ∈ range i, normalizedForcing a b f k)
          ≤ ∑ k ∈ range i, C * r ^ k := by
        exact Finset.sum_le_sum (fun k _ => h_term_upper k)
      _ = C * (∑ k ∈ range i, r ^ k) := by
        simp [Finset.mul_sum]
      _ ≤ C * (1 - r)⁻¹ := by
        gcongr
        exact geometric_sum_le_tsum_bound hr_nonneg hr_lt_one i
  rcases hsum_bound with ⟨B, hB_nonneg, hB⟩
  have h_lower :
      ∃ c : ℝ, 0 < c ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ →
        c * (fun _ : ℕ => (1 : ℝ)) i ≤ normalizedValue a b T i := by
    refine ⟨normalizedValue a b T 0, h_base_pos, 0, ?_⟩
    intro i _hi
    have h_formula_i :=
      normalizedValue_eq_base_add_sum a b f T h_rec ha_ne_zero i
    have hsum_nonneg : 0 ≤ ∑ k ∈ range i, normalizedForcing a b f k :=
      Finset.sum_nonneg (fun k _ => h_term_nonneg k)
    calc
      normalizedValue a b T 0 * (1 : ℝ) = normalizedValue a b T 0 := by ring
      _ ≤ normalizedValue a b T i := by
        rw [h_formula_i]
        linarith
  have h_upper :
      ∃ C' : ℝ, 0 < C' ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ →
        normalizedValue a b T i ≤ C' * (fun _ : ℕ => (1 : ℝ)) i := by
    refine ⟨normalizedValue a b T 0 + B, by linarith, 0, ?_⟩
    intro i _hi
    have h_formula_i :=
      normalizedValue_eq_base_add_sum a b f T h_rec ha_ne_zero i
    calc
      normalizedValue a b T i =
          normalizedValue a b T 0 + (∑ k ∈ range i, normalizedForcing a b f k) := h_formula_i
      _ ≤ normalizedValue a b T 0 + B := by
        gcongr
        exact hB i
      _ = (normalizedValue a b T 0 + B) * (1 : ℝ) := by ring
  simpa using
    theta_of_normalized_by_scale a b T (fun _ : ℕ => (1 : ℝ)) ha_pos
      (fun _ => by norm_num) h_lower h_upper

Master case 2, exact-power form: if the normalized forcing terms are trapped between positive constants, then T(b^i) = Θ((i+1)a^i).


theorem master_case2_constant_forcing (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (ha_pos : 0 < (a : ℝ))
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ k, c ≤ normalizedForcing a b f k)
    (h_term_upper : ∀ k, normalizedForcing a b f k ≤ C) :
    Chapter03.isBigTheta
      (fun i : ℕ => T (b ^ i))
      (fun i : ℕ => ((i : ℝ) + 1) * ((a : ℝ) ^ i)) := by
  have ha_ne_zero : (a : ℝ) ≠ 0 := ne_of_gt ha_pos
  refine theta_of_normalized_by_scale a b T (fun i => (i : ℝ) + 1) ha_pos
    (fun i => by positivity) ?_ ?_
  · refine ⟨c / 2, by positivity, 1, ?_⟩
    intro i hi
    have h_formula_i :=
      normalizedValue_eq_base_add_sum a b f T h_rec ha_ne_zero i
    have hsum_lower :
        c * (i : ℝ) ≤ ∑ k ∈ range i, normalizedForcing a b f k := by
      calc
        c * (i : ℝ) = ∑ _k ∈ range i, c := by
          simp [Finset.sum_const, nsmul_eq_mul, mul_comm]
        _ ≤ ∑ k ∈ range i, normalizedForcing a b f k := by
          exact Finset.sum_le_sum (fun k _ => h_term_lower k)
    have hi_real : 1 ≤ (i : ℝ) := by exact_mod_cast hi
    calc
      (c / 2) * ((i : ℝ) + 1) ≤ c * (i : ℝ) := by nlinarith [hc_pos]
      _ ≤ ∑ k ∈ range i, normalizedForcing a b f k := hsum_lower
      _ ≤ normalizedValue a b T i := by
        rw [h_formula_i]
        linarith
  · refine ⟨normalizedValue a b T 0 + C, by linarith, 0, ?_⟩
    intro i _hi
    have h_formula_i :=
      normalizedValue_eq_base_add_sum a b f T h_rec ha_ne_zero i
    have hsum_upper :
        (∑ k ∈ range i, normalizedForcing a b f k) ≤ C * (i : ℝ) := by
      calc
        (∑ k ∈ range i, normalizedForcing a b f k) ≤ ∑ _k ∈ range i, C := by
          exact Finset.sum_le_sum (fun k _ => h_term_upper k)
        _ = C * (i : ℝ) := by
          simp [Finset.sum_const, nsmul_eq_mul, mul_comm]
    have hi_nonneg : 0 ≤ (i : ℝ) := by positivity
    calc
      normalizedValue a b T i =
          normalizedValue a b T 0 + (∑ k ∈ range i, normalizedForcing a b f k) := h_formula_i
      _ ≤ normalizedValue a b T 0 + C * (i : ℝ) := by
        gcongr
      _ ≤ (normalizedValue a b T 0 + C) * ((i : ℝ) + 1) := by
        nlinarith [h_base_nonneg, hC_pos]

Case 2 with a polylog factor

The sum of the first i nonnegative k-th powers is at least (i/2)^(k+1): the terms at indices i/2, ..., i-1 each contribute at least (i/2)^k.


private lemma sum_pow_ge_half_pow (i k : ℕ) (hi : 2 ≤ i) :
    ((i / 2 : ℕ) : ℝ) ^ (k + 1) ≤ ∑ j ∈ Finset.range i, (j : ℝ) ^ k := by
  let S : Finset ℕ := Finset.Icc (i / 2) (i - 1)
  have hsub : S ⊆ Finset.range i := by
    intro j hj
    rw [Finset.mem_Icc] at hj
    rw [Finset.mem_range]
    omega
  have hsum_sub : (∑ j ∈ S, (j : ℝ) ^ k) ≤ ∑ j ∈ Finset.range i, (j : ℝ) ^ k := by
    exact Finset.sum_le_sum_of_subset_of_nonneg hsub (fun j _ _ => pow_nonneg (by positivity) _)
  have hmin : ∀ j ∈ S, ((i / 2 : ℕ) : ℝ) ^ k ≤ (j : ℝ) ^ k := by
    intro j hj
    rw [Finset.mem_Icc] at hj
    exact pow_le_pow_left₀ (by positivity : 0 ≤ ((i / 2 : ℕ) : ℝ))
      (by exact_mod_cast hj.1) k
  have hcard_ge : ((i / 2 : ℕ) : ℝ) ≤ (S.card : ℝ) := by
    have hcard : S.card = i - i / 2 := by
      rw [Nat.card_Icc]
      omega
    have hge : (i / 2 : ℕ) ≤ i - i / 2 := by omega
    rw [hcard]
    exact_mod_cast hge
  have hsum_min : (S.card : ℝ) * ((i / 2 : ℕ) : ℝ) ^ k ≤ ∑ j ∈ S, (j : ℝ) ^ k := by
    calc
      (S.card : ℝ) * ((i / 2 : ℕ) : ℝ) ^ k = ∑ _j ∈ S, ((i / 2 : ℕ) : ℝ) ^ k := by
        simp [Finset.sum_const, nsmul_eq_mul]
      _ ≤ ∑ j ∈ S, (j : ℝ) ^ k := by
        exact Finset.sum_le_sum (fun j hj => hmin j hj)
  calc
    ((i / 2 : ℕ) : ℝ) ^ (k + 1) = ((i / 2 : ℕ) : ℝ) * ((i / 2 : ℕ) : ℝ) ^ k := by
      rw [pow_succ']
    _ ≤ (S.card : ℝ) * ((i / 2 : ℕ) : ℝ) ^ k := by
      exact mul_le_mul_of_nonneg_right hcard_ge (by positivity)
    _ ≤ ∑ j ∈ S, (j : ℝ) ^ k := hsum_min
    _ ≤ ∑ j ∈ Finset.range i, (j : ℝ) ^ k := hsum_sub

The sum of the first i nonnegative k-th powers is Θ(i^(k+1)); this is the lower-bound half in terms of (i+1)^(k+1).


private lemma sum_pow_ge (i k : ℕ) (hi : 2 ≤ i) :
    (1 / 4 ^ (k + 1) : ℝ) * ((i : ℝ) + 1) ^ (k + 1) ≤
      ∑ j ∈ Finset.range i, (j : ℝ) ^ k := by
  have hhalf := sum_pow_ge_half_pow i k hi
  have h4 : ((i / 2 : ℕ) : ℝ) ≥ ((i : ℝ) + 1) / 4 := by
    have hnat : (i / 2 : ℕ) * 4 ≥ i + 1 := by omega
    have hcast : ((i / 2 : ℕ) : ℝ) * 4 ≥ (i : ℝ) + 1 := by exact_mod_cast hnat
    linarith
  have hrel : (1 / 4 ^ (k + 1) : ℝ) * ((i : ℝ) + 1) ^ (k + 1) ≤
      ((i / 2 : ℕ) : ℝ) ^ (k + 1) := by
    calc
      (1 / 4 ^ (k + 1) : ℝ) * ((i : ℝ) + 1) ^ (k + 1) = (((i : ℝ) + 1) / 4) ^ (k + 1) := by
        rw [div_pow]
        field_simp
      _ ≤ ((i / 2 : ℕ) : ℝ) ^ (k + 1) := by
        exact pow_le_pow_left₀ (by positivity : 0 ≤ ((i : ℝ) + 1) / 4) h4 (k + 1)
  exact le_trans hrel hhalf

The sum of the first i nonnegative k-th powers is at most (i+1)^(k+1): each of the i terms is at most i^k.


private lemma sum_pow_le (i k : ℕ) :
    (∑ j ∈ Finset.range i, (j : ℝ) ^ k) ≤ ((i : ℝ) + 1) ^ (k + 1) := by
  calc
    (∑ j ∈ Finset.range i, (j : ℝ) ^ k) ≤ ∑ _j ∈ Finset.range i, (i : ℝ) ^ k := by
      exact Finset.sum_le_sum (fun j hj => pow_le_pow_left₀ (by positivity) (by
        rw [Finset.mem_range] at hj
        exact_mod_cast (Nat.le_of_lt hj)) k)
    _ = (i : ℝ) * (i : ℝ) ^ k := by
      simp [Finset.sum_const, nsmul_eq_mul]
    _ = (i : ℝ) ^ (k + 1) := by rw [pow_succ', mul_comm]
    _ ≤ ((i : ℝ) + 1) ^ (k + 1) := by
      exact pow_le_pow_left₀ (by positivity) (by linarith) (k + 1)

Master case 2 with a polylog factor, exact-power form: if the normalized forcing terms grow polynomially, c·j^k ≤ normalizedForcing a b f j ≤ C·j^k, then T(b^i) = Θ((i+1)^(k+1)·a^i).

For f(n) = Θ(n^(log_b a)·log^k n) the normalized forcing is Θ(j^k), so this is the standard textbook extension T(n) = Θ(n^(log_b a)·log^(k+1) n); the k = 0 case recovers master_case2_constant_forcing.


theorem master_case2_polylog_forcing (a b k : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (ha_pos : 0 < (a : ℝ))
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    {c C : ℝ} (hc_pos : 0 < c) (hC_pos : 0 < C)
    (h_term_lower : ∀ j : ℕ, c * (j : ℝ) ^ k ≤ normalizedForcing a b f j)
    (h_term_upper : ∀ j : ℕ, normalizedForcing a b f j ≤ C * (j : ℝ) ^ k) :
    Chapter03.isBigTheta
      (fun i : ℕ => T (b ^ i))
      (fun i : ℕ => (((i : ℝ) + 1) ^ (k + 1)) * ((a : ℝ) ^ i)) := by
  have ha_ne_zero : (a : ℝ) ≠ 0 := ne_of_gt ha_pos
  refine theta_of_normalized_by_scale a b T (fun i => ((i : ℝ) + 1) ^ (k + 1)) ha_pos
    (fun i => by positivity) ?_ ?_
  · refine ⟨c / 4 ^ (k + 1), by positivity, 2, ?_⟩
    intro i hi
    have h_formula_i := normalizedValue_eq_base_add_sum a b f T h_rec ha_ne_zero i
    have hsum_lower :
        c * (1 / 4 ^ (k + 1) : ℝ) * ((i : ℝ) + 1) ^ (k + 1) ≤
          ∑ j ∈ range i, normalizedForcing a b f j := by
      calc
        c * (1 / 4 ^ (k + 1) : ℝ) * ((i : ℝ) + 1) ^ (k + 1)
            ≤ c * (∑ j ∈ range i, (j : ℝ) ^ k) := by
              simpa [mul_assoc] using mul_le_mul_of_nonneg_left (sum_pow_ge i k hi) hc_pos.le
        _ = ∑ j ∈ range i, c * (j : ℝ) ^ k := by
          simp [Finset.mul_sum]
        _ ≤ ∑ j ∈ range i, normalizedForcing a b f j := by
          exact Finset.sum_le_sum (fun j hj => h_term_lower j)
    calc
      (c / 4 ^ (k + 1) : ℝ) * ((i : ℝ) + 1) ^ (k + 1)
          = c * (1 / 4 ^ (k + 1) : ℝ) * ((i : ℝ) + 1) ^ (k + 1) := by ring
      _ ≤ ∑ j ∈ range i, normalizedForcing a b f j := hsum_lower
      _ ≤ normalizedValue a b T i := by
        rw [h_formula_i]
        linarith
  · refine ⟨normalizedValue a b T 0 + C, by linarith, 0, ?_⟩
    intro i _hi
    have h_formula_i := normalizedValue_eq_base_add_sum a b f T h_rec ha_ne_zero i
    have hsum_upper :
        (∑ j ∈ range i, normalizedForcing a b f j) ≤ C * ((i : ℝ) + 1) ^ (k + 1) := by
      calc
        (∑ j ∈ range i, normalizedForcing a b f j) ≤ ∑ j ∈ range i, C * (j : ℝ) ^ k := by
          exact Finset.sum_le_sum (fun j hj => h_term_upper j)
        _ = C * (∑ j ∈ range i, (j : ℝ) ^ k) := by
          simp [Finset.mul_sum]
        _ ≤ C * ((i : ℝ) + 1) ^ (k + 1) := by
          exact mul_le_mul_of_nonneg_left (sum_pow_le i k) hC_pos.le
    have hi_nonneg : 0 ≤ (i : ℝ) := by positivity
    have hscale_ge : (1 : ℝ) ≤ ((i : ℝ) + 1) ^ (k + 1) := by
      have hbase : (1 : ℝ) ≤ (i : ℝ) + 1 := by linarith
      have hpow := pow_le_pow_left₀ (by norm_num : (0 : ℝ) ≤ 1) hbase (k + 1)
      simpa using hpow
    calc
      normalizedValue a b T i =
          normalizedValue a b T 0 + (∑ j ∈ range i, normalizedForcing a b f j) := h_formula_i
      _ ≤ normalizedValue a b T 0 + C * ((i : ℝ) + 1) ^ (k + 1) := by
        gcongr
      _ ≤ (normalizedValue a b T 0 + C) * ((i : ℝ) + 1) ^ (k + 1) := by
        have hbase_le : normalizedValue a b T 0 ≤
            normalizedValue a b T 0 * ((i : ℝ) + 1) ^ (k + 1) := by
          exact le_mul_of_one_le_right h_base_nonneg hscale_ge
        nlinarith

Master case 3, exact-power form: if the normalized recurrence value is eventually controlled by the last normalized forcing term, then the last term dominates the whole recurrence tree. This is a conditional criterion; normalized_tail_upper_of_eventual_regularity derives its upper-bound premise from forcing regularity, and master_case3_of_eventual_regularity states the resulting exact-power theorem directly in terms of f.


theorem master_case3_tail_dominated (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (ha_pos : 0 < (a : ℝ))
    (h_base_nonneg : 0 ≤ normalizedValue a b T 0)
    (h_term_nonneg : ∀ k, 0 ≤ normalizedForcing a b f k)
    (h_tail_upper :
      ∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ → 1 ≤ i →
        normalizedValue a b T i ≤ C * normalizedForcing a b f (i - 1)) :
    Chapter03.isBigTheta
      (fun i : ℕ => T (b ^ i))
      (fun i : ℕ =>
        (if i = 0 then 1 else normalizedForcing a b f (i - 1)) * ((a : ℝ) ^ i)) := by
  have ha_ne_zero : (a : ℝ) ≠ 0 := ne_of_gt ha_pos
  refine theta_of_normalized_by_scale a b T
    (fun i : ℕ => if i = 0 then 1 else normalizedForcing a b f (i - 1))
    ha_pos ?_ ?_ ?_
  · intro i
    by_cases hi : i = 0
    · simp [hi]
    · simp [hi, h_term_nonneg]
  · refine ⟨1, by norm_num, 1, ?_⟩
    intro i hi
    have hi_pos : 0 < i := by omega
    have hi_ne : i ≠ 0 := Nat.ne_of_gt hi_pos
    have h_formula_i :=
      normalizedValue_eq_base_add_sum a b f T h_rec ha_ne_zero i
    have hlast_mem : i - 1 ∈ range i := by
      rw [Finset.mem_range]
      omega
    have hlast_le_sum :
        normalizedForcing a b f (i - 1) ≤
          ∑ k ∈ range i, normalizedForcing a b f k :=
      Finset.single_le_sum (fun k _ => h_term_nonneg k) hlast_mem
    calc
      1 * (if i = 0 then 1 else normalizedForcing a b f (i - 1))
          = normalizedForcing a b f (i - 1) := by simp [hi_ne]
      _ ≤ ∑ k ∈ range i, normalizedForcing a b f k := hlast_le_sum
      _ ≤ normalizedValue a b T i := by
        rw [h_formula_i]
        linarith
  · rcases h_tail_upper with ⟨C, hC_pos, n₀, htail⟩
    refine ⟨C, hC_pos, max 1 n₀, ?_⟩
    intro i hi
    have hi_one : 1 ≤ i := le_trans (Nat.le_max_left _ _) hi
    have hi_n₀ : i ≥ n₀ := le_trans (Nat.le_max_right _ _) hi
    have hi_ne : i ≠ 0 := by omega
    calc
      normalizedValue a b T i ≤ C * normalizedForcing a b f (i - 1) :=
        htail i hi_n₀ hi_one
      _ = C * (if i = 0 then 1 else normalizedForcing a b f (i - 1)) := by simp [hi_ne]

Case 3 from forcing regularity

Eventual forcing regularity controls the recurrence itself. The finite prefix is absorbed in the constant chosen at index i₀; no upper bound on T is assumed. Positivity at that index is needed to absorb its cost.


theorem exactPower_upper_of_eventual_regularity (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (i₀ : ℕ) {c : ℝ}
    (hc_lt_one : c < 1)
    (hf_start : 0 < f (b ^ i₀))
    (hf_nonneg : ∀ i, i₀ ≤ i → 0 ≤ f (b ^ i))
    (h_reg : ∀ i, i₀ ≤ i → (a : ℝ) * f (b ^ i) ≤ c * f (b ^ (i + 1))) :
    ∃ K : ℝ, 0 < K ∧ ∀ i, i₀ ≤ i → T (b ^ i) ≤ K * f (b ^ i) := by
  let K : ℝ := max (T (b ^ i₀) / f (b ^ i₀)) (1 / (1 - c))
  have hd : 0 < 1 - c := sub_pos.mpr hc_lt_one
  have hK_inv : 1 / (1 - c) ≤ K := le_max_right _ _
  have hK_pos : 0 < K := lt_of_lt_of_le (div_pos zero_lt_one hd) hK_inv
  have hK_step : K * c + 1 ≤ K := by
    have := (div_le_iff₀ hd).mp hK_inv
    nlinarith
  refine ⟨K, hK_pos, ?_⟩
  intro i hi
  induction i, hi using Nat.le_induction with
  | base =>
      exact (div_le_iff₀ hf_start).mp (le_max_left _ _)
  | succ i hi ih =>
      calc
        T (b ^ (i + 1)) = (a : ℝ) * T (b ^ i) + f (b ^ (i + 1)) :=
          h_rec.step i
        _ ≤ (a : ℝ) * (K * f (b ^ i)) + f (b ^ (i + 1)) := by
          gcongr
        _ = K * ((a : ℝ) * f (b ^ i)) + f (b ^ (i + 1)) := by ring
        _ ≤ K * (c * f (b ^ (i + 1))) + f (b ^ (i + 1)) := by
          exact add_le_add
            (mul_le_mul_of_nonneg_left (h_reg i hi) hK_pos.le) le_rfl
        _ = (K * c + 1) * f (b ^ (i + 1)) := by ring
        _ ≤ K * f (b ^ (i + 1)) :=
          mul_le_mul_of_nonneg_right hK_step (hf_nonneg _ (by omega))

The normalized tail-upper premise of master_case3_tail_dominated follows from eventual forcing regularity. This bridge also supplies the premise required by the existing floor/ceiling all-input wrappers.

theorem normalized_tail_upper_of_eventual_regularity
    (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (i₀ : ℕ) {c : ℝ}
    (hc_lt_one : c < 1)
    (hf_start : 0 < f (b ^ i₀))
    (hf_nonneg : ∀ i, i₀ ≤ i → 0 ≤ f (b ^ i))
    (h_reg : ∀ i, i₀ ≤ i → (a : ℝ) * f (b ^ i) ≤ c * f (b ^ (i + 1))) :
    ∃ K : ℝ, 0 < K ∧ ∃ n₀ : ℕ, ∀ i, i ≥ n₀ → 1 ≤ i →
      normalizedValue a b T i ≤ K * normalizedForcing a b f (i - 1) := by
  obtain ⟨K, hK, hbound⟩ :=
    exactPower_upper_of_eventual_regularity a b f T h_rec i₀ hc_lt_one
      hf_start hf_nonneg h_reg
  refine ⟨K, hK, i₀, ?_⟩
  intro i hi hi_one
  simpa [normalizedValue, normalizedForcing, Nat.sub_add_cancel hi_one, mul_div_assoc]
    using div_le_div_of_nonneg_right (hbound i hi) (pow_nonneg (Nat.cast_nonneg a) i)

Master case 3 on exact powers, derived from eventual forcing regularity a f(b^i) ≤ c f(b^(i+1)), with c < 1. Nonnegative costs and one positive forcing value after the threshold suffice; arbitrary finite prefixes are allowed. The conclusion uses the original forcing function.

The usual 0 ≤ c condition may be omitted: the proof only needs c < 1 together with the stated forcing signs.


theorem master_case3_of_eventual_regularity (a b : ℕ) (f T : ℕ → ℝ)
    (h_rec : ExactPowerRecurrence a b f T) (i₀ : ℕ) {c : ℝ}
    (hc_lt_one : c < 1) (h_base_nonneg : 0 ≤ T 1)
    (hf_start : 0 < f (b ^ i₀))
    (hf_nonneg : ∀ i, 0 ≤ f (b ^ i))
    (h_reg : ∀ i, i₀ ≤ i → (a : ℝ) * f (b ^ i) ≤ c * f (b ^ (i + 1))) :
    Chapter03.isBigTheta (fun i : ℕ => T (b ^ i)) (fun i : ℕ => f (b ^ i)) := by
  have hT_nonneg : ∀ i, 0 ≤ T (b ^ i) := by
    intro i
    induction i with
    | zero => simpa using h_base_nonneg
    | succ i ih =>
        rw [h_rec.step i]
        exact add_nonneg (mul_nonneg (Nat.cast_nonneg a) ih) (hf_nonneg _)
  obtain ⟨K, hK, hbound⟩ :=
    exactPower_upper_of_eventual_regularity a b f T h_rec i₀ hc_lt_one
      hf_start (fun i _ => hf_nonneg i) h_reg
  refine isBigTheta_of_eventual_bounds ⟨K, hK, i₀, ?_⟩ ⟨1, zero_lt_one, 1, ?_⟩
  · intro i hi
    simpa [abs_of_nonneg (hT_nonneg i), abs_of_nonneg (hf_nonneg i)] using hbound i hi
  · intro i hi
    obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : i ≠ 0)
    rw [abs_of_nonneg (hT_nonneg _), abs_of_nonneg (hf_nonneg _), one_mul,
      h_rec.step j]
    exact le_add_of_nonneg_left (mul_nonneg (Nat.cast_nonneg a) (hT_nonneg j))

end Chapter04end CLRS