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

Imports

import CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.TextbookExamples
import CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.IntegerTree

open Finsetopen scoped BigOperators

4.4. The Recursion-Tree Method for Solving Recurrences

This file makes the finite-sum core of the CLRS recursion-tree method explicit.

Main results:

Theorem CLRS.Chapter04.recursion_tree_additive_unroll: an additive one-step recurrence is exactly the base value plus the sum of level costs.
Theorem CLRS.Chapter04.recursion_tree_additive_upper_envelope: if each level cost is bounded by an envelope, the whole tree is bounded by the sum of the envelope.
Theorem CLRS.Chapter04.recursion_tree_constant_level_cost: constant level costs give the usual linear closed form.
Theorem CLRS.Chapter04.BranchingRecursionTree.totalCost_eq_levelCosts_add_leafCost: an explicit finite branching tree decomposes into internal level costs plus leaf costs.
Theorems CLRS.Chapter04.balancedThreeQuarter_totalCost_le and CLRS.Chapter04.unbalancedThirdTwoThird_totalCost: the two detailed textbook examples have respectively geometric and constant level costs.
Theorem CLRS.Chapter04.IntegerBranchingSpec.build_totalCost_eq: an explicit finite natural-size tree has exactly the value of its independently stated floor/ceiling recurrence, even when branches stop at unequal depths.
Theorems CLRS.Chapter04.balancedIntegerTree_totalCost_eq and CLRS.Chapter04.unbalancedIntegerTree_totalCost_eq: arbitrary-input integer instances of the two detailed textbook examples.
Theorems CLRS.Chapter04.balancedIntegerCost_isBigTheta and CLRS.Chapter04.unbalancedIntegerCost_isBigTheta: actual rounded-tree total costs are Θ(n²) and Θ(n log n) for positive local-cost coefficients and nonnegative base costs.

Status: proved for the finite-sum core, the fixed-depth level-sum model, and the explicit unequal-depth integer floor/ceiling trees. The exact tree semantics equal independently stated rounded recurrences. Strong induction on these recurrences proves the two actual execution bounds, including unequal child depths. This does not claim a general theorem for arbitrary rounded branching recurrences.

namespace CLRSnamespace Chapter04

Unroll an additive recurrence into the sum of its level costs.


theorem recursion_tree_additive_unroll (T cost : ℕ → ℝ)
    (hstep : ∀ n, T (n + 1) = T n + cost n) (n : ℕ) :
    T n = T 0 + ∑ k ∈ range n, cost k := by
  induction n with
  | zero =>
      simp
  | succ n ih =>
      rw [hstep n, ih]
      simp [sum_range_succ, add_assoc]

If every level cost is bounded by an envelope, then the unrolled recursion tree is bounded by the sum of that envelope.


theorem recursion_tree_additive_upper_envelope (T cost envelope : ℕ → ℝ)
    (hcost : ∀ k, cost k ≤ envelope k)
    (hstep : ∀ n, T (n + 1) = T n + cost n) (n : ℕ) :
    T n ≤ T 0 + ∑ k ∈ range n, envelope k := by
  rw [recursion_tree_additive_unroll T cost hstep n]
  exact add_le_add le_rfl (Finset.sum_le_sum (fun k _hk => hcost k))

If every level cost is at least an envelope, then the same unrolling gives a lower bound by the envelope sum.


theorem recursion_tree_additive_lower_envelope (T cost envelope : ℕ → ℝ)
    (hcost : ∀ k, envelope k ≤ cost k)
    (hstep : ∀ n, T (n + 1) = T n + cost n) (n : ℕ) :
    T 0 + ∑ k ∈ range n, envelope k ≤ T n := by
  rw [recursion_tree_additive_unroll T cost hstep n]
  exact add_le_add le_rfl (Finset.sum_le_sum (fun k _hk => hcost k))

Constant level costs collapse the recursion tree to the base value plus a linear term.


theorem recursion_tree_constant_level_cost (T : ℕ → ℝ) {level : ℝ}
    (hstep : ∀ n, T (n + 1) = T n + level) :
    ∀ n : ℕ, T n = T 0 + level * (n : ℝ) := by
  intro n
  rw [recursion_tree_additive_unroll T (fun _ => level) hstep n]
  simp [Finset.sum_const, nsmul_eq_mul, mul_comm]

A bounded-cost recursion tree with at most level work per depth is bounded by the base bound plus level * n.

theorem recursion_tree_constant_upper_bound (T cost : ℕ → ℝ) {base level : ℝ}
    (hbase : T 0 ≤ base)
    (hcost : ∀ k, cost k ≤ level)
    (hstep : ∀ n, T (n + 1) = T n + cost n) :
    ∀ n : ℕ, T n ≤ base + level * (n : ℝ) := by
  intro n
  have hsum := recursion_tree_additive_upper_envelope T cost (fun _ => level) hcost hstep n
  calc
    T n ≤ T 0 + ∑ _k ∈ range n, level := hsum
    _ ≤ base + ∑ _k ∈ range n, level := by linarith
    _ = base + level * (n : ℝ) := by
      simp [Finset.sum_const, nsmul_eq_mul, mul_comm]

end Chapter04end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.IntegerTree.Asymptotics

Connections to Chapter 4 asymptotic interfaces

The costs of the generated rounded trees satisfy the textbook bounds on all natural inputs: the balanced tree has quadratic cost, and the unequal-depth tree has Θ(n log n) cost. The proofs use their actual recurrence equations, including the floor and ceiling operations and base cases.

namespace CLRSnamespace Chapter04

The integer unequal-depth example uses the classic Akra--Bazzi root p=1.

theorem unbalancedInteger_akraBazziRoot :
    IsAkraBazziRoot [(1, (3 : Real)), (1, (3 : Real) / 2)] 1 :=
  akraBazziRoot_two_thirds_one

The balanced tree has nonnegative cost and a quadratic upper potential, including zero-size leaves.


theorem balancedIntegerCost_bounds {c base : ℝ} (hc : 0 ≤ c) (hb : 0 ≤ base)
    (n : ℕ) :
    0 ≤ balancedIntegerCost c base n ∧
      balancedIntegerCost c base n ≤ (4*c+base)*((n : ℝ)+1)^2 := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hn : n ≤ 1
      · rw [balancedIntegerCost_base hn]
        constructor
        · exact hb
        · have hsq : 1 ≤ ((n : ℝ)+1)^2 := by nlinarith [Nat.cast_nonneg (α := ℝ) n]
          have hmul := mul_le_mul_of_nonneg_left hsq (show 0 ≤ 4*c+base by positivity)
          nlinarith
      · have hn' : 1 < n := by omega
        have hq : n/4 < n := Nat.div_lt_self (by omega) (by norm_num)
        obtain ⟨hl, hu⟩ := ih (n/4) hq
        rw [balancedIntegerCost_step hn']
        constructor
        · positivity
        · have hhalfNat : 2*(n/4+1) ≤ n+1 := by omega
          have hhalf : 2*((n/4 : ℕ)+1 : ℝ) ≤ (n : ℝ)+1 := by exact_mod_cast hhalfNat
          have hq0 : 0 ≤ ((n/4 : ℕ) : ℝ) := by positivity
          have hn0 : 0 ≤ (n : ℝ) := by positivity
          have hK0 : 0 ≤ 4*c+base := by positivity
          have hsq : 4*(((n/4 : ℕ) : ℝ)+1)^2 ≤ ((n : ℝ)+1)^2 := by nlinarith
          have hw := mul_le_mul_of_nonneg_left hsq hK0
          have hlocal := mul_nonneg hc
            (show 0 ≤ ((n : ℝ)+1)^2-(n : ℝ)^2 by nlinarith)
          have hbase := mul_nonneg hb (sq_nonneg ((n : ℝ)+1))
          nlinarith

The generated balanced rounded tree has Θ(n²) cost whenever its quadratic local charge is positive and its leaf charge is nonnegative.


theorem balancedIntegerCost_isBigTheta {c base : ℝ} (hc : 0 < c) (hb : 0 ≤ base) :
    Chapter03.isBigTheta (balancedIntegerCost c base) (fun n : ℕ => (n : ℝ)^2) := by
  constructor
  · apply (Chapter03.isBigO_iff _ _).mpr
    refine ⟨4*(4*c+base), by positivity, 2, ?_⟩
    intro n hn
    obtain ⟨hl, hu⟩ := balancedIntegerCost_bounds hc.le hb n
    rw [abs_of_nonneg hl, abs_of_nonneg (sq_nonneg _)]
    have hn1 : 1 ≤ (n : ℝ) := by exact_mod_cast (show 1 ≤ n by omega)
    have hsq : ((n : ℝ)+1)^2 ≤ 4*(n : ℝ)^2 := by nlinarith
    have hw := mul_le_mul_of_nonneg_left hsq (show 0 ≤ 4*c+base by positivity)
    nlinarith
  · apply (Chapter03.isBigOmega_iff _ _).mpr
    refine ⟨c, hc, 2, ?_⟩
    intro n hn
    rw [abs_of_nonneg (balancedIntegerCost_bounds hc.le hb n).1,
      abs_of_nonneg (sq_nonneg _), balancedIntegerCost_step (by omega)]
    have hchild := (balancedIntegerCost_bounds hc.le hb (n/4)).1
    linarith



private theorem rounded_thirds_bounds (n : ℕ) (hn : 2 < n) :
    n/3 + twoThirdsCeil n = n ∧ 0 < n/3 ∧ 0 < twoThirdsCeil n ∧
      n ≤ 5*(n/3) ∧ n ≤ 5*twoThirdsCeil n ∧
      5*(n/3) ≤ 4*n ∧ 5*twoThirdsCeil n ≤ 4*n := by
  rw [twoThirdsCeil, Nat.ceilDiv_eq_add_pred_div]
  by_cases hsmall : n < 6
  · interval_cases n <;> norm_num at *
  · omega



private theorem split_log_gap (n x y : ℝ) (hx : 0 < x) (hy : 0 < y)
    (hs : x+y=n) (hlx : n ≤ 5*x) (hly : n ≤ 5*y)
    (hux : 5*x ≤ 4*n) (huy : 5*y ≤ 4*n) :
    n/5 ≤ n*Real.log n-x*Real.log x-y*Real.log y ∧
      n*Real.log n-x*Real.log x-y*Real.log y ≤ 4*n := by
  have hn : 0 < n := by linarith
  have hlogLow : (1:ℝ)/5 ≤ Real.log ((5:ℝ)/4) := by
    have h := Real.one_sub_inv_le_log_of_pos (x := (5:ℝ)/4) (by norm_num)
    norm_num at h ⊢
    exact h
  have hlogHigh : Real.log (5:ℝ) ≤ 4 := by
    have h := Real.log_le_sub_one_of_pos (x := (5:ℝ)) (by norm_num)
    norm_num at h ⊢
    exact h
  have hlogs (z : ℝ) (hz : 0 < z) (hl : n ≤ 5*z) (hu : 5*z ≤ 4*n) :
      (1:ℝ)/5 ≤ Real.log n-Real.log z ∧ Real.log n-Real.log z ≤ 4 := by
    have hlo : (5:ℝ)/4 ≤ n/z := (le_div_iff₀ hz).mpr (by nlinarith)
    have hhi : n/z ≤ 5 := (div_le_iff₀ hz).mpr hl
    rw [← Real.log_div hn.ne' hz.ne']
    exact ⟨hlogLow.trans (Real.log_le_log (by norm_num) hlo),
      (Real.log_le_log (div_pos hn hz) hhi).trans hlogHigh⟩
  have hxl := mul_le_mul_of_nonneg_left (hlogs x hx hlx hux).1 hx.le
  have hxu := mul_le_mul_of_nonneg_left (hlogs x hx hlx hux).2 hx.le
  have hyl := mul_le_mul_of_nonneg_left (hlogs y hy hly huy).1 hy.le
  have hyu := mul_le_mul_of_nonneg_left (hlogs y hy hly huy).2 hy.le
  have heq : n*Real.log n-x*Real.log x-y*Real.log y =
      x*(Real.log n-Real.log x)+y*(Real.log n-Real.log y) := by
    rw [← hs]
    ring
  rw [heq]
  constructor <;> nlinarith

Explicit affine logarithmic potentials for the actual unequal-depth tree. The linear terms absorb the base cases and cancel at each rounded split.


theorem unbalancedIntegerCost_bounds {c base : ℝ} (hc : 0 ≤ c) (hb : 0 ≤ base)
    (n : ℕ) (hn : 1 ≤ n) :
    0 ≤ unbalancedIntegerCost c base n ∧
      (c/4)*(n : ℝ)*(Real.log (n : ℝ)-1) ≤ unbalancedIntegerCost c base n ∧
      unbalancedIntegerCost c base n ≤ 5*c*(n : ℝ)*Real.log (n : ℝ)+base*(n : ℝ) := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hbase : n ≤ 2
      · rw [unbalancedIntegerCost_base hbase]
        have hlog2 : Real.log (2:ℝ) ≤ 1 := by
          have h := Real.log_le_sub_one_of_pos (x := (2:ℝ)) (by norm_num)
          norm_num at h ⊢
          exact h
        have hlog2pos : 0 ≤ Real.log (2:ℝ) := Real.log_nonneg (by norm_num)
        interval_cases n <;> norm_num at *
        · exact ⟨hb, by nlinarith⟩
        · exact ⟨hb, by nlinarith [mul_nonneg hc (sub_nonneg.mpr hlog2)],
            by nlinarith [mul_nonneg hc hlog2pos]⟩
      · have hrec : 2 < n := by omega
        obtain ⟨hs, hx, hy, hlx, hly, hux, huy⟩ := rounded_thirds_bounds n hrec
        have hsR : ((n/3 : ℕ) : ℝ)+(twoThirdsCeil n : ℝ)=(n : ℝ) := by exact_mod_cast hs
        have hgap := split_log_gap (n : ℝ) ((n/3 : ℕ) : ℝ) (twoThirdsCeil n : ℝ)
          (by exact_mod_cast hx) (by exact_mod_cast hy) hsR
          (by exact_mod_cast hlx) (by exact_mod_cast hly)
          (by exact_mod_cast hux) (by exact_mod_cast huy)
        obtain ⟨hx0, hxL, hxU⟩ := ih (n/3) (thirdFloor_lt_self hrec) (by omega)
        obtain ⟨hy0, hyL, hyU⟩ := ih (twoThirdsCeil n) (twoThirdsCeil_lt_self hrec) (by omega)
        rw [unbalancedIntegerCost_step hrec]
        refine ⟨by positivity, ?_, ?_⟩
        · have hw := mul_le_mul_of_nonneg_left hgap.2 (show 0 ≤ c/4 by positivity)
          have hcancel : (c/4)*((n/3 : ℕ) : ℝ)+(c/4)*(twoThirdsCeil n : ℝ)=
              (c/4)*(n : ℝ) := by rw [← mul_add, hsR]
          nlinarith
        · have hw := mul_le_mul_of_nonneg_left hgap.1 (show 0 ≤ 5*c by positivity)
          have hcancel : base*((n/3 : ℕ) : ℝ)+base*(twoThirdsCeil n : ℝ)=
              base*(n : ℝ) := by rw [← mul_add, hsR]
          nlinarith



private theorem two_le_log_of_sixteen_le {n : ℕ} (hn : 16 ≤ n) :
    2 ≤ Real.log (n : ℝ) := by
  have hhalf := Real.one_sub_inv_le_log_of_pos (x := (2:ℝ)) (by norm_num)
  have hm := Real.log_le_log (by norm_num : (0:ℝ)<16) (show (16:ℝ) ≤ n by exact_mod_cast hn)
  have hpow : Real.log (16:ℝ) = 4*Real.log (2:ℝ) := by
    rw [show (16:ℝ)=2^4 by norm_num, Real.log_pow]
    norm_num
  rw [hpow] at hm
  norm_num at hhalf
  linarith

The generated floor/ceiling unequal-depth tree has Θ(n log n) cost. This follows from its recurrence and rounding arithmetic, without an assumed asymptotic comparison or an Akra--Bazzi certificate.


theorem unbalancedIntegerCost_isBigTheta {c base : ℝ} (hc : 0 < c) (hb : 0 ≤ base) :
    Chapter03.isBigTheta (unbalancedIntegerCost c base)
      (fun n : ℕ => (n : ℝ)*Real.log (n : ℝ)) := by
  constructor
  · apply (Chapter03.isBigO_iff _ _).mpr
    refine ⟨5*c+base, by positivity, 16, ?_⟩
    intro n hn
    obtain ⟨h0, _, hU⟩ := unbalancedIntegerCost_bounds hc.le hb n (by omega)
    have hlog := two_le_log_of_sixteen_le hn
    rw [abs_of_nonneg h0, abs_of_nonneg (by positivity)]
    have hw := mul_nonneg (mul_nonneg hb (Nat.cast_nonneg n))
      (show 0 ≤ Real.log (n : ℝ)-1 by linarith)
    nlinarith
  · apply (Chapter03.isBigOmega_iff _ _).mpr
    refine ⟨c/8, by positivity, 16, ?_⟩
    intro n hn
    obtain ⟨h0, hL, _⟩ := unbalancedIntegerCost_bounds hc.le hb n (by omega)
    have hlog := two_le_log_of_sixteen_le hn
    rw [abs_of_nonneg h0, abs_of_nonneg (by positivity)]
    have hw := mul_nonneg (mul_nonneg hc.le (Nat.cast_nonneg n))
      (show 0 ≤ Real.log (n : ℝ)-2 by linarith)
    nlinarith

end Chapter04end CLRS

CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.IntegerTree.Balanced

The integer tree for `3T(n/4) + c n²`

This is the rounded, arbitrary-input counterpart of the existing fixed-depth real-scale level calculation.

              namespace CLRSnamespace Chapter04open Finsetopen scoped BigOperators

Three equal floor-divided children, with base cases at sizes zero and one.

def balancedIntegerSpec (c base : Real) : IntegerBranchingSpec (Fin 3) where
  cutoff := 1
  childSize := fun _ n => n / 4
  localCost := fun n => c * (n : Real) ^ 2
  baseCost := fun _ => base
  decreases := by
    intro _ n hn
    exact Nat.div_lt_self (by omega) (by norm_num)

Independent textbook equations for the rounded balanced recurrence.

structure BalancedIntegerRecurrence (c base : Real) (T : Nat → Real) : Prop where
  base_eq : ∀ n, n ≤ 1 → T n = base
  step_eq : ∀ n, 1 < n →
    T n = 3 * T (n / 4) + c * (n : Real) ^ 2

The textbook equations instantiate the generic finite-tree semantics.


theorem BalancedIntegerRecurrence.satisfies {c base : Real} {T : Nat → Real}
    (hT : BalancedIntegerRecurrence c base T) :
    (balancedIntegerSpec c base).Satisfies T := by
  constructor
  · intro n hn
    exact hT.base_eq n hn
  · intro n hn
    rw [hT.step_eq n hn]
    simp [balancedIntegerSpec]
    ring

Exact equality between the rounded recurrence and its explicit tree.

theorem balancedIntegerTree_totalCost_eq {c base : Real} {T : Nat → Real}
    (hT : BalancedIntegerRecurrence c base T) (n : Nat) :
    IntegerBranchingTree.totalCost ((balancedIntegerSpec c base).build n) = T n :=
  IntegerBranchingSpec.build_totalCost_eq _ _ hT.satisfies n

Cost function computed by the generated balanced integer tree.

def balancedIntegerCost (c base : Real) (n : Nat) : Real :=
  IntegerBranchingTree.totalCost ((balancedIntegerSpec c base).build n)

              @[simp] theorem balancedIntegerCost_base {c base : Real} {n : Nat}
    (hn : n ≤ 1) : balancedIntegerCost c base n = base := by
  simp [balancedIntegerCost, balancedIntegerSpec, hn]

theorem balancedIntegerCost_step {c base : Real} {n : Nat}
    (hn : 1 < n) :
    balancedIntegerCost c base n =
      3 * balancedIntegerCost c base (n / 4) + c * (n : Real) ^ 2 := by
  rw [balancedIntegerCost, IntegerBranchingSpec.build_of_lt _ _ hn]
  simp only [IntegerBranchingTree.totalCost_node]
  simp [balancedIntegerSpec, balancedIntegerCost]
  ringtheorem balancedIntegerCost_satisfies (c base : Real) :
    BalancedIntegerRecurrence c base (balancedIntegerCost c base) := by
  constructor
  · intro n hn
    exact balancedIntegerCost_base hn
  · intro n hn
    exact balancedIntegerCost_step hn

Forcing term that makes the generated tree cost an all-input floor recurrence, including the explicitly represented base cases.

def balancedIntegerForcing (c base : Real) (n : Nat) : Real :=
  balancedIntegerCost c base n - 3 * balancedIntegerCost c base (n / 4)

Direct connection from the explicit tree to the all-input §4.6 interface.

theorem balancedIntegerCost_floorRecurrence (c base : Real) :
    FloorDivideRecurrence 3 4 (balancedIntegerForcing c base)
      (balancedIntegerCost c base) := by
  constructor
  intro n
  simp [balancedIntegerForcing]

Above the cutoff, the all-input forcing is exactly the textbook c n².


theorem balancedIntegerForcing_of_lt {c base : Real} {n : Nat} (hn : 1 < n) :
    balancedIntegerForcing c base n = c * (n : Real) ^ 2 := by
  rw [balancedIntegerForcing, balancedIntegerCost_step hn]
  ring

end Chapter04end CLRS

CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.IntegerTree.Execution

Building integer branching trees

A specification contains the termination proof for every rounded child. The recurrence equation is stated independently, then strong induction identifies its solution with the cost of the generated finite tree.

              namespace CLRSnamespace Chapter04open Finsetopen scoped BigOperators

Data needed to expand a natural-size recurrence into a finite tree.

structure IntegerBranchingSpec (Branch : Type) where
  cutoff : Nat
  childSize : Branch → Nat → Nat
  localCost : Nat → Real
  baseCost : Nat → Real
  decreases : ∀ branch n, cutoff < n → childSize branch n < n

namespace IntegerBranchingSpecvariable {Branch : Type}

The recurrence semantics, stated without referring to the generated tree.

structure Satisfies [Fintype Branch] (spec : IntegerBranchingSpec Branch)
    (T : Nat → Real) : Prop where
  base : ∀ n, n ≤ spec.cutoff → T n = spec.baseCost n
  step : ∀ n, spec.cutoff < n →
    T n = spec.localCost n + ∑ branch, T (spec.childSize branch n)

Executably expand all children until their independently certified cutoff.

def build (spec : IntegerBranchingSpec Branch) (n : Nat) :
    IntegerBranchingTree Branch :=
  if _h : n ≤ spec.cutoff then
    .leaf n (spec.baseCost n)
  else
    .node n (spec.localCost n) (fun branch => spec.build (spec.childSize branch n))
termination_by n
decreasing_by
  exact spec.decreases _ _ (Nat.lt_of_not_ge _h)



@[simp] theorem build_of_le (spec : IntegerBranchingSpec Branch) (n : Nat)
    (h : n ≤ spec.cutoff) :
    spec.build n = .leaf n (spec.baseCost n) := by
  rw [build]
  simp [h]



@[simp] theorem build_of_lt (spec : IntegerBranchingSpec Branch) (n : Nat)
    (h : spec.cutoff < n) :
    spec.build n = .node n (spec.localCost n)
      (fun branch => spec.build (spec.childSize branch n)) := by
  rw [build]
  simp [Nat.not_le_of_gt h]

Building preserves the requested root subproblem size.

@[simp] theorem rootSize_build (spec : IntegerBranchingSpec Branch) (n : Nat) :
    IntegerBranchingTree.rootSize (spec.build n) = n := by
  by_cases h : n ≤ spec.cutoff
  · simp [build_of_le spec n h]
  · simp [build_of_lt spec n (Nat.lt_of_not_ge h)]

Predicate saying that every leaf size satisfies a given property.

def EveryLeafSize (P : Nat → Prop) : IntegerBranchingTree Branch → Prop
  | .leaf size _ => P size
  | .node _ _ children => ∀ branch, EveryLeafSize P (children branch)

Predicate saying that every internal-node size satisfies a property.

def EveryInternalSize (P : Nat → Prop) : IntegerBranchingTree Branch → Prop
  | .leaf _ _ => True
  | .node size _ children => P size ∧ ∀ branch, EveryInternalSize P (children branch)

Every generated leaf is genuinely in the base-case range.


theorem build_everyLeaf_le (spec : IntegerBranchingSpec Branch) (n : Nat) :
    EveryLeafSize (fun size => size ≤ spec.cutoff) (spec.build n) := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hbase : n ≤ spec.cutoff
      · simp [EveryLeafSize, hbase]
      · have hrec : spec.cutoff < n := Nat.lt_of_not_ge hbase
        rw [build_of_lt spec n hrec]
        simp only [EveryLeafSize]
        intro branch
        exact ih (spec.childSize branch n) (spec.decreases branch n hrec)

Every generated internal node is genuinely above the cutoff.


theorem build_everyInternal_gt (spec : IntegerBranchingSpec Branch) (n : Nat) :
    EveryInternalSize (fun size => spec.cutoff < size) (spec.build n) := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hbase : n ≤ spec.cutoff
      · simp [build_of_le spec n hbase, EveryInternalSize]
      · have hrec : spec.cutoff < n := Nat.lt_of_not_ge hbase
        rw [build_of_lt spec n hrec]
        simp only [EveryInternalSize]
        refine ⟨hrec, fun branch => ?_⟩
        exact ih (spec.childSize branch n) (spec.decreases branch n hrec)

Exact recurrence-tree semantics. This is not true by definition: T is specified only by its base and recursive equations, independently of build.


theorem build_totalCost_eq [Fintype Branch] (spec : IntegerBranchingSpec Branch)
    (T : Nat → Real) (hT : spec.Satisfies T) (n : Nat) :
    IntegerBranchingTree.totalCost (spec.build n) = T n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      by_cases hbase : n ≤ spec.cutoff
      · rw [build_of_le spec n hbase]
        simp [hT.base n hbase]
      · have hrec : spec.cutoff < n := Nat.lt_of_not_ge hbase
        rw [build_of_lt spec n hrec]
        simp only [IntegerBranchingTree.totalCost_node]
        have hchildren : ∀ branch,
            IntegerBranchingTree.totalCost
                (spec.build (spec.childSize branch n)) =
              T (spec.childSize branch n) := fun branch =>
          ih (spec.childSize branch n) (spec.decreases branch n hrec)
        simp_rw [hchildren]
        exact (hT.step n hrec).symm

              end IntegerBranchingSpecend Chapter04end CLRS

CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.IntegerTree.Model

Unequal-depth integer branching trees

This datatype records the actual natural-number size and work of every node. It is intentionally not indexed by a common depth: floor and ceiling branches may reach the base case at different times.

              namespace CLRSnamespace Chapter04open Finsetopen scoped BigOperators

A finite recursion tree whose branches need not have the same height.

inductive IntegerBranchingTree (Branch : Type)
  | leaf (size : Nat) (work : Real)
  | node (size : Nat) (work : Real)
      (children : Branch → IntegerBranchingTree Branch)

namespace IntegerBranchingTreevariable {Branch : Type}

Natural-number subproblem size stored at the root.

def rootSize : IntegerBranchingTree Branch → Nat
  | .leaf size _ => size
  | .node size _ _ => size

Work stored at the root, whether it is a base or recursive node.

def rootWork : IntegerBranchingTree Branch → Real
  | .leaf _ work => work
  | .node _ work _ => work

Work stored in every node of the finite tree.

def totalCost [Fintype Branch] : IntegerBranchingTree Branch → Real
  | .leaf _ work => work
  | .node _ work children => work + ∑ branch, totalCost (children branch)

Maximum number of recursive edges on a root-to-leaf path.

def height [Fintype Branch] [DecidableEq Branch] :
    IntegerBranchingTree Branch → Nat
  | .leaf _ _ => 0
  | .node _ _ children => 1 + Finset.univ.sup (fun branch => height (children branch))

              @[simp] theorem rootSize_leaf (size : Nat) (work : Real) :
    rootSize (.leaf size work : IntegerBranchingTree Branch) = size := rfl@[simp] theorem rootSize_node (size : Nat) (work : Real)
    (children : Branch → IntegerBranchingTree Branch) :
    rootSize (.node size work children) = size := rfl@[simp] theorem rootWork_leaf (size : Nat) (work : Real) :
    rootWork (.leaf size work : IntegerBranchingTree Branch) = work := rfl@[simp] theorem rootWork_node (size : Nat) (work : Real)
    (children : Branch → IntegerBranchingTree Branch) :
    rootWork (.node size work children) = work := rfl@[simp] theorem totalCost_leaf [Fintype Branch] (size : Nat) (work : Real) :
    totalCost (.leaf size work : IntegerBranchingTree Branch) = work := rfl@[simp] theorem totalCost_node [Fintype Branch] (size : Nat) (work : Real)
    (children : Branch → IntegerBranchingTree Branch) :
    totalCost (.node size work children) =
      work + ∑ branch, totalCost (children branch) := rfl@[simp] theorem height_leaf [Fintype Branch] [DecidableEq Branch]
    (size : Nat) (work : Real) :
    height (.leaf size work : IntegerBranchingTree Branch) = 0 := rfl@[simp] theorem height_node [Fintype Branch] [DecidableEq Branch]
    (size : Nat) (work : Real)
    (children : Branch → IntegerBranchingTree Branch) :
    height (.node size work children) =
      1 + Finset.univ.sup (fun branch => height (children branch)) := rflend IntegerBranchingTreeend Chapter04end CLRS

CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.IntegerTree.Unbalanced

The integer tree for `T(n/3) + T(2n/3) + c n`

The larger child uses natural ceiling division. The generated tree therefore has no artificial common depth.

              namespace CLRSnamespace Chapter04open Finsetopen scoped BigOperators

The textbook rounded size ceil(2n/3).

def twoThirdsCeil (n : Nat) : Nat :=
  (2 * n) ⌈/⌉ 3

The smaller floor branch decreases above the chosen cutoff.

theorem thirdFloor_lt_self {n : Nat} (hn : 2 < n) : n / 3 < n := by
  exact Nat.div_lt_self (by omega) (by norm_num)

The larger ceiling branch also decreases above the chosen cutoff.


theorem twoThirdsCeil_lt_self {n : Nat} (hn : 2 < n) : twoThirdsCeil n < n := by
  rw [twoThirdsCeil, Nat.ceilDiv_eq_add_pred_div]
  omega

Floor and ceiling differ by at most one for the two-thirds child.


theorem twoThirds_floor_ceil_sandwich (n : Nat) :
    (2 * n) / 3 ≤ twoThirdsCeil n ∧
      twoThirdsCeil n ≤ (2 * n) / 3 + 1 := by
  constructor
  · rw [twoThirdsCeil, Nat.ceilDiv_eq_add_pred_div]
    omega
  · rw [twoThirdsCeil, Nat.ceilDiv_eq_add_pred_div]
    omega

Two differently rounded children, with base cases through size two.

def unbalancedIntegerSpec (c base : Real) : IntegerBranchingSpec Bool where
  cutoff := 2
  childSize := fun branch n => if branch then twoThirdsCeil n else n / 3
  localCost := fun n => c * (n : Real)
  baseCost := fun _ => base
  decreases := by
    intro branch n hn
    cases branch with
    | false =>
        simpa using thirdFloor_lt_self hn
    | true =>
        simpa using twoThirdsCeil_lt_self hn

Independent textbook equations for the rounded unbalanced recurrence.

structure UnbalancedIntegerRecurrence (c base : Real) (T : Nat → Real) : Prop where
  base_eq : ∀ n, n ≤ 2 → T n = base
  step_eq : ∀ n, 2 < n →
    T n = T (n / 3) + T (twoThirdsCeil n) + c * (n : Real)

The textbook equations instantiate the generic finite-tree semantics.


theorem UnbalancedIntegerRecurrence.satisfies {c base : Real} {T : Nat → Real}
    (hT : UnbalancedIntegerRecurrence c base T) :
    (unbalancedIntegerSpec c base).Satisfies T := by
  constructor
  · intro n hn
    exact hT.base_eq n hn
  · intro n hn
    rw [hT.step_eq n hn]
    simp [unbalancedIntegerSpec]
    ring

Exact equality between the rounded recurrence and its explicit tree.

theorem unbalancedIntegerTree_totalCost_eq {c base : Real} {T : Nat → Real}
    (hT : UnbalancedIntegerRecurrence c base T) (n : Nat) :
    IntegerBranchingTree.totalCost ((unbalancedIntegerSpec c base).build n) = T n :=
  IntegerBranchingSpec.build_totalCost_eq _ _ hT.satisfies n

Cost function computed by the generated unbalanced integer tree.

def unbalancedIntegerCost (c base : Real) (n : Nat) : Real :=
  IntegerBranchingTree.totalCost ((unbalancedIntegerSpec c base).build n)

              @[simp] theorem unbalancedIntegerCost_base {c base : Real} {n : Nat}
    (hn : n ≤ 2) : unbalancedIntegerCost c base n = base := by
  simp [unbalancedIntegerCost, unbalancedIntegerSpec, hn]

theorem unbalancedIntegerCost_step {c base : Real} {n : Nat}
    (hn : 2 < n) :
    unbalancedIntegerCost c base n =
      unbalancedIntegerCost c base (n / 3) +
        unbalancedIntegerCost c base (twoThirdsCeil n) + c * (n : Real) := by
  rw [unbalancedIntegerCost, IntegerBranchingSpec.build_of_lt _ _ hn]
  simp only [IntegerBranchingTree.totalCost_node]
  simp [unbalancedIntegerSpec, unbalancedIntegerCost]
  ringtheorem unbalancedIntegerCost_satisfies (c base : Real) :
    UnbalancedIntegerRecurrence c base (unbalancedIntegerCost c base) := by
  constructor
  · intro n hn
    exact unbalancedIntegerCost_base hn
  · intro n hn
    exact unbalancedIntegerCost_step hn

At input four, the floor(4/3) child is already a leaf while the ceil(8/3) child expands once more. This witnesses genuinely unequal depth.


theorem unbalancedIntegerTree_has_unequal_depth :
    IntegerBranchingTree.height
        ((unbalancedIntegerSpec 1 1).build
          ((unbalancedIntegerSpec 1 1).childSize false 4)) ≠
      IntegerBranchingTree.height
        ((unbalancedIntegerSpec 1 1).build
          ((unbalancedIntegerSpec 1 1).childSize true 4)) := by
  have hleft : (unbalancedIntegerSpec 1 1).childSize false 4 = 1 := by
    norm_num [unbalancedIntegerSpec]
  have hright : (unbalancedIntegerSpec 1 1).childSize true 4 = 3 := by
    norm_num [unbalancedIntegerSpec, twoThirdsCeil, Nat.ceilDiv_eq_add_pred_div]
  rw [hleft, hright]
  have hheightOne : IntegerBranchingTree.height
      ((unbalancedIntegerSpec 1 1).build 1) = 0 := by
    rw [IntegerBranchingSpec.build_of_le _ _ (by norm_num [unbalancedIntegerSpec])]
    rfl
  have hheightThree : IntegerBranchingTree.height
      ((unbalancedIntegerSpec 1 1).build 3) = 1 := by
    rw [IntegerBranchingSpec.build_of_lt _ _ (by norm_num [unbalancedIntegerSpec])]
    simp [IntegerBranchingTree.height, unbalancedIntegerSpec, twoThirdsCeil]
  omega

The limiting one-third and two-thirds branch weights sum to one.

theorem unbalancedInteger_characteristic_one :
    (1 : Real) / 3 + 2 / 3 = 1 := by
  norm_num

end Chapter04end CLRS

CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.LevelSums

Reusable branching level sums

This file builds a full recursion tree from per-branch work-scaling ratios and proves its exact per-level cost. It also packages the convergent geometric sum bound used by the balanced textbook example.

              namespace CLRSnamespace Chapter04open Finsetopen scoped BigOperatorsopen BranchingRecursionTreevariable {Branch : Type} [Fintype Branch]

A homogeneous branching expansion. A child on branch branch receives ratios branch times its parent's local work. Leaves have a common cutoff cost; this parameter is intentionally separate from the internal work scale.

def scaledBranchingTree (ratios : Branch -> Real) (rootWork leafWork : Real) :
    (depth : Nat) -> BranchingRecursionTree Branch depth
  | 0 => .leaf leafWork
  | depth + 1 => .node rootWork (fun branch =>
      scaledBranchingTree ratios (rootWork * ratios branch) leafWork depth)

At level k, the total work is the root work times the kth power of the sum of the per-branch work ratios.


theorem scaledBranchingTree_levelCost (ratios : Branch -> Real)
    (rootWork leafWork : Real) {depth : Nat} (level : Fin depth) :
    levelCost (scaledBranchingTree ratios rootWork leafWork depth) level =
      rootWork * (∑ branch, ratios branch) ^ level.val := by
  induction depth generalizing rootWork with
  | zero => exact Fin.elim0 level
  | succ depth ih =>
      refine Fin.cases ?_ (fun childLevel => ?_) level
      · simp [scaledBranchingTree, levelCost]
      · simp only [scaledBranchingTree, levelCost, Fin.cases_succ]
        simp_rw [ih]
        rw [← Finset.sum_mul, ← Finset.mul_sum]
        simp only [Fin.val_succ, pow_succ]
        ring

A full depth-d expansion has card Branch ^ d leaves.

theorem scaledBranchingTree_leafCost (ratios : Branch -> Real)
    (rootWork leafWork : Real) (depth : Nat) :
    leafCost (scaledBranchingTree ratios rootWork leafWork depth) =
      (Fintype.card Branch : Real) ^ depth * leafWork := by
  induction depth generalizing rootWork with
  | zero => simp [scaledBranchingTree, leafCost]
  | succ depth ih =>
      simp [scaledBranchingTree, leafCost, ih, Finset.sum_const, nsmul_eq_mul,
        pow_succ]
      ring

Exact closed form of the full branching expansion through a fixed depth.


theorem scaledBranchingTree_totalCost (ratios : Branch -> Real)
    (rootWork leafWork : Real) (depth : Nat) :
    totalCost (scaledBranchingTree ratios rootWork leafWork depth) =
      (∑ level : Fin depth,
        rootWork * (∑ branch, ratios branch) ^ level.val) +
      (Fintype.card Branch : Real) ^ depth * leafWork := by
  rw [totalCost_eq_levelCosts_add_leafCost]
  simp_rw [scaledBranchingTree_levelCost]
  rw [scaledBranchingTree_leafCost]

A reusable finite geometric level-sum bound.


theorem geometricLevelSum_le (base ratio : Real) (hbase : 0 <= base)
    (hratio_nonneg : 0 <= ratio) (hratio_lt_one : ratio < 1) (depth : Nat) :
    (∑ level ∈ Finset.range depth, base * ratio ^ level) <=
      base / (1 - ratio) := by
  have hsumm : Summable fun level : Nat => ratio ^ level :=
    summable_geometric_of_lt_one hratio_nonneg hratio_lt_one
  have hpartial : (∑ level ∈ Finset.range depth, ratio ^ level) <=
      (1 - ratio)⁻¹ := by
    calc
      (∑ level ∈ Finset.range depth, ratio ^ level) <= ∑' level : Nat, ratio ^ level :=
        hsumm.sum_le_tsum (Finset.range depth)
          (fun level _ => pow_nonneg hratio_nonneg level)
      _ = (1 - ratio)⁻¹ :=
        tsum_geometric_of_lt_one hratio_nonneg hratio_lt_one
  calc
    (∑ level ∈ Finset.range depth, base * ratio ^ level) =
        base * ∑ level ∈ Finset.range depth, ratio ^ level := by
      rw [Finset.mul_sum]
    _ <= base * (1 - ratio)⁻¹ := mul_le_mul_of_nonneg_left hpartial hbase
    _ = base / (1 - ratio) := by rw [div_eq_mul_inv]

end Chapter04end CLRS

CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.Model

Full branching recursion trees

BranchingRecursionTree Branch depth is an explicit, finite expansion of a branching recurrence through exactly depth internal levels. Every internal node has one child for each value of the finite type Branch; all leaves lie at the same cutoff depth. This is the exact-power / fixed-depth model used in the textbook level-cost calculation. Floor and ceiling transfer for arbitrary input sizes is deliberately a separate concern.

              namespace CLRSnamespace Chapter04open Finsetopen scoped BigOperators

A full finite branching recursion tree with depth internal levels.

inductive BranchingRecursionTree (Branch : Type) : Nat -> Type
  | leaf (cost : Real) : BranchingRecursionTree Branch 0
  | node {depth : Nat} (work : Real)
      (children : Branch -> BranchingRecursionTree Branch depth) :
      BranchingRecursionTree Branch (depth + 1)

namespace BranchingRecursionTreevariable {Branch : Type} [Fintype Branch]

Total work stored in all internal nodes and leaves.

def totalCost : {depth : Nat} -> BranchingRecursionTree Branch depth -> Real
  | 0, .leaf cost => cost
  | _ + 1, .node work children => work + ∑ branch, totalCost (children branch)

Total contribution of the leaves at the cutoff depth.

def leafCost : {depth : Nat} -> BranchingRecursionTree Branch depth -> Real
  | 0, .leaf cost => cost
  | _ + 1, .node _ children => ∑ branch, leafCost (children branch)

Work contributed by the internal nodes at one depth.

def levelCost : {depth : Nat} -> (tree : BranchingRecursionTree Branch depth) ->
    Fin depth -> Real
  | 0, .leaf _, level => Fin.elim0 level
  | _ + 1, .node work children, level =>
      Fin.cases work (fun childLevel =>
        ∑ branch, levelCost (children branch) childLevel) level

Exact recursion-tree decomposition: total cost is the sum of all internal level costs plus the cost of the leaves at the common cutoff depth.


theorem totalCost_eq_levelCosts_add_leafCost {depth : Nat}
    (tree : BranchingRecursionTree Branch depth) :
    totalCost tree = (∑ level : Fin depth, levelCost tree level) + leafCost tree := by
  induction tree with
  | leaf cost => simp [totalCost, leafCost]
  | @node depth work children ih =>
      simp only [totalCost, leafCost]
      rw [Fin.sum_univ_succ]
      simp only [levelCost, Fin.cases_zero, Fin.cases_succ]
      simp_rw [ih]
      rw [Finset.sum_add_distrib]
      rw [Finset.sum_comm]
      ring

              end BranchingRecursionTreeend Chapter04end CLRS

CLRSLean.FourthEdition.Chapter_04.Section_04_4_Recursion_Tree_Method.Branching.TextbookExamples

Textbook branching-recursion-tree examples

The theorems below are exact fixed-depth expansions over real-valued problem scales. They formalize the level-cost calculations from CLRS §4.4 while keeping the assumptions visible:

no floor or ceiling is taken at a child size;
all branches are expanded through a common cutoff depth;
leafWork is the common cost assigned at that cutoff.

Consequently these results are the recursion-tree algebra for the original branch ratios, not an arbitrary-input termination theorem. A transfer from these exact scales to rounded natural-number recurrences needs separate monotonicity and floor/ceiling bounds.

              namespace CLRSnamespace Chapter04open Finsetopen scoped BigOperatorsopen BranchingRecursionTree

The balanced example `3T(n/4) + c n^2`

The fixed-depth recursion tree for 3T(n/4) + c n^2. Quadratic local work scales by 1/16 on each of the three child branches.

noncomputable def balancedThreeQuarterTree (c n leafWork : Real) (depth : Nat) :
    BranchingRecursionTree (Fin 3) depth :=
  scaledBranchingTree (fun _ : Fin 3 => (1 : Real) / 16) (c * n ^ 2) leafWork depth

At level k, the balanced example costs exactly c n^2 (3/16)^k.


theorem balancedThreeQuarter_levelCost (c n leafWork : Real) {depth : Nat}
    (level : Fin depth) :
    levelCost (balancedThreeQuarterTree c n leafWork depth) level =
      c * n ^ 2 * ((3 : Real) / 16) ^ level.val := by
  rw [balancedThreeQuarterTree, scaledBranchingTree_levelCost]
  norm_num

Exact internal-level plus leaf decomposition for the balanced example.


theorem balancedThreeQuarter_totalCost_eq (c n leafWork : Real) (depth : Nat) :
    totalCost (balancedThreeQuarterTree c n leafWork depth) =
      (∑ level : Fin depth,
        c * n ^ 2 * ((3 : Real) / 16) ^ level.val) +
      (3 : Real) ^ depth * leafWork := by
  rw [balancedThreeQuarterTree, scaledBranchingTree_totalCost]
  norm_num

The internal work of 3T(n/4) + c n^2 is bounded by the convergent geometric sum 16/13 * c n^2; the leaf contribution remains explicit.


theorem balancedThreeQuarter_totalCost_le (c n leafWork : Real)
    (hc : 0 <= c) (depth : Nat) :
    totalCost (balancedThreeQuarterTree c n leafWork depth) <=
      ((16 : Real) / 13) * (c * n ^ 2) + (3 : Real) ^ depth * leafWork := by
  have hbase : 0 <= c * n ^ 2 := mul_nonneg hc (sq_nonneg n)
  have hlevels := geometricLevelSum_le (c * n ^ 2) ((3 : Real) / 16)
    hbase (by norm_num) (by norm_num) depth
  have hlevelsFin :
      (∑ level : Fin depth, c * n ^ 2 * ((3 : Real) / 16) ^ level.val) <=
        (c * n ^ 2) / (1 - (3 : Real) / 16) := by
    rw [Fin.sum_univ_eq_sum_range
      (fun level : Nat => c * n ^ 2 * ((3 : Real) / 16) ^ level) depth]
    exact hlevels
  rw [balancedThreeQuarter_totalCost_eq]
  calc
    (∑ level : Fin depth, c * n ^ 2 * ((3 : Real) / 16) ^ level.val) +
          (3 : Real) ^ depth * leafWork <=
        (c * n ^ 2) / (1 - (3 : Real) / 16) +
          (3 : Real) ^ depth * leafWork := add_le_add hlevelsFin le_rfl
    _ = ((16 : Real) / 13) * (c * n ^ 2) +
          (3 : Real) ^ depth * leafWork := by ring

The unbalanced example `T(n/3) + T(2n/3) + c n`

The two exact child-work ratios for the linear-work unbalanced recurrence.

noncomputable def thirdTwoThirdRatio : Bool -> Real
  | false => (1 : Real) / 3
  | true => (2 : Real) / 3

A common-depth expansion of T(n/3) + T(2n/3) + c n.

The two child trees retain their different 1/3 and 2/3 scales; they are not replaced by a balanced recurrence.

noncomputable def unbalancedThirdTwoThirdTree (c n leafWork : Real) (depth : Nat) :
    BranchingRecursionTree Bool depth :=
  scaledBranchingTree thirdTwoThirdRatio (c * n) leafWork depth

Since 1/3 + 2/3 = 1, every internal level in the common-depth expansion has exactly the root's linear work c n.


theorem unbalancedThirdTwoThird_levelCost (c n leafWork : Real) {depth : Nat}
    (level : Fin depth) :
    levelCost (unbalancedThirdTwoThirdTree c n leafWork depth) level = c * n := by
  rw [unbalancedThirdTwoThirdTree, scaledBranchingTree_levelCost]
  have hratio : (∑ branch : Bool, thirdTwoThirdRatio branch) = (1 : Real) := by
    norm_num [thirdTwoThirdRatio]
  rw [hratio, one_pow, mul_one]

Exact total cost through a common cutoff depth: depth * c n internal work plus one leafWork contribution for each of the 2^depth leaves.

This theorem is deliberately not advertised as an arbitrary-size solution: the actual 1/3 and 2/3 branches reach a natural-number base threshold at different depths after rounding.


theorem unbalancedThirdTwoThird_totalCost (c n leafWork : Real) (depth : Nat) :
    totalCost (unbalancedThirdTwoThirdTree c n leafWork depth) =
      (depth : Real) * (c * n) + (2 : Real) ^ depth * leafWork := by
  rw [unbalancedThirdTwoThirdTree, scaledBranchingTree_totalCost]
  have hratio : (∑ branch : Bool, thirdTwoThirdRatio branch) = (1 : Real) := by
    norm_num [thirdTwoThirdRatio]
  rw [hratio]
  simp [nsmul_eq_mul]

end Chapter04end CLRS

4.4. The Recursion-Tree Method for Solving Recurrences

Definitions and proofs

Connections to Chapter 4 asymptotic interfaces

The integer tree for 3T(n/4) + c n²

Building integer branching trees

Unequal-depth integer branching trees

The integer tree for T(n/3) + T(2n/3) + c n

Reusable branching level sums

Full branching recursion trees

Textbook branching-recursion-tree examples

The balanced example 3T(n/4) + c n^2

The unbalanced example T(n/3) + T(2n/3) + c n

The integer tree for `3T(n/4) + c n²`

The integer tree for `T(n/3) + T(2n/3) + c n`

The balanced example `3T(n/4) + c n^2`

The unbalanced example `T(n/3) + T(2n/3) + c n`