Skip to content
  1. CLRS-Lean
  2. Chapters 1–35 · CLRS Fourth Edition
  3. Chapter 4. Divide-and-Conquer
  4. 4.7. Akra–Bazzi Recurrences
Browse chapters
Imports
import CLRSLean.FourthEdition.Chapter_04.Section_04_6_Continuous_Master_Theorem
open scoped BigOperators

4.7. Akra–Bazzi Recurrences

The Akra–Bazzi method (CLRS §4.7) solves divide-and-conquer recurrences of the form

  T(n) = Σ_i a_i · T(n / b_i) + g(n)

whose recursion tree is not uniformly branching. The method first finds the unique exponent p solving the root equation Σ_i a_i b_i^(-p) = 1, then bounds T(n) by Θ(n^p (1 + ∫₁ⁿ g(u) / u^(p+1) du)).

This section formalizes the recurrence hypotheses, the root equation and its scale n^p, proves that a single branch recovers the continuous master theorem of §4.6 (root p = log_b a), proves the multi-branch root is unique and nonnegative, proves the fundamental scale-invariance bridge Σᵢ aᵢ (n/bᵢ)^p = n^p, records the classic two-branch instance T(n) = T(n/3) + T(2n/3) + n whose root is p = 1, and lays out the integral asymptotic form with its explicit polynomial-smoothness predicate.

Main results:

  • Definition charTerm / charFun: the characteristic term a / b^p and the characteristic function Σ a_i / b_i^p.

  • Definition IsAkraBazziRoot: the root equation Σ a_i / b_i^p = 1.

  • Theorem akraBazziRoot_single: a single branch (a, b) has root p = log_b a, the continuous master-theorem exponent.

  • Theorem akraBazziRoot_single_unique: the root is unique.

  • Theorem akraBazziRoot_two_thirds_one: the two-branch instance T(n) = T(n/3) + T(2n/3) has root p = 1.

  • Theorem akraBazzi_single_branch_corollary: the single-branch root and its scale n^p coincide with the discrete CLRS.­Chapter04.­realLogScale used by the continuous master theorem.

  • Theorem akraBazziRoot_unique: the multi-branch root is unique.

  • Theorem akraBazziRoot_nonneg: the multi-branch root is nonnegative.

  • Theorem akraBazzi_root_scale_invariance: the fundamental multi-branch bridge Σᵢ aᵢ (n/bᵢ)^p = n^p.

  • Definition akraBazziIntegral / akraBazziScale: the discrete integral Σ_{u=1}^n g(u)/u^(p+1) and the scale n^p (1 + Σ_{u≤n} g(u)/u^(p+1)).

  • Definition PolynomialGrowth: the explicit polynomial-smoothness predicate c n^q ≤ g n ≤ C n^q with monotonicity and nonnegativity.

  • Definition SatisfiesAkraBazzi: the recurrence T(n) = Σᵢ aᵢ T(⌊n/bᵢ⌋) + g(n) with floor perturbation and a constant base case.

  • Theorems akraBazziIntegral_mono, akraBazziIntegral_sub, akraBazziIntegral_lower_const, and akraBazziIntegral_bounded_of_lt: the integral's monotonicity, its tail decomposition, its positive lower bound, and its boundedness for q < p (the convergent p-series).

  • Theorems akraBazziIntegral_tail_lower and akraBazzi_increment_lower: the integral tail is at least its number of terms times its smallest term, and the single-branch increment a (n/b)^p (I n - I ⌊n/b⌋) dominates g n by a positive factor — the analytic core of the upper-bound substitution proof.

  • Definition akraBazziIncrement: the per-branch increment a (n/b)^p (I n - I ⌊n/b⌋).

  • Theorems akraBazziIntegral_tail_upper, akraBazzi_increment_upper_single, akraBazzi_increment_upper, and akraBazzi_increment_lower_multi: the multi-branch increment is bounded above and below by a positive constant times g n.

  • Theorem akraBazzi_scale_decomp: the children's scales sum to the scale minus the total increment.

  • Theorem akraBazzi_T_nonneg: a solution is nonnegative.

  • Theorem akraBazzi_T_ge_g: above the base threshold, g n ≤ T n.

  • Theorems akraBazzi_upper_bound_nonneg and akraBazzi_upper_bound: the solution is O(n^p (1 + I n)), the upper recurrence-to-integral comparison.

  • Theorem akraBazzi_lower_bound: the solution is Ω(n^p (1 + I n)) when p + 1 ≤ q, the lower comparison in the forcing-dominated regime.

  • Theorem akraBazzi_lower_bound_critical: the solution is Ω(n^p (1 + I n)) when q = p, the lower comparison in the critical regime, established by the substitution induction with the power floor loss absorbed by the driving term.

  • Theorem akraBazzi_bigTheta_critical: the critical upper and lower comparisons packaged as the textbook Θ(n^p (1 + I n)) conclusion.

  • Theorem akraBazzi_bigTheta: the full Θ(n^p (1 + I n)) bound when p + 1 ≤ q.

  • Definition akraBazziSmoothingFn: the smoothing function ε x = 1 / √x, whose drop dominates the one-step floor loss.

  • Lemma akraBazzi_smoothing_scale_floor_ge: the floored smoothing scale ⌊n/b⌋^p (1 + ε⌊n/b⌋) is eventually a subsolution of the homogeneous recurrence — the discrete analogue of the Kuszmaul–Leiserson smoothing step.

  • Theorem akraBazzi_lower_bound_leaf: the solution is Ω(n^p (1 + I n)) when 0 ≤ q < p, the lower comparison in the deep leaf-dominated regime, closed by the smoothing factor.

  • Theorem akraBazzi_bigTheta_leaf: the full Θ(n^p (1 + I n)) bound when 0 ≤ q < p.

Status: proved for the root equation, the single-branch corollary (which recovers the master theorem), the multi-branch root uniqueness/nonnegativity, the scale-invariance bridge, the integral machinery, the two-sided increment bounds, and the recurrence-to-integral comparison in both directions — the upper bound T(n) = O(n^p(1+I n)) for arbitrary p ≥ 0, q ≥ 0, and the matching lower bound T(n) = Ω(n^p(1+I n)) (hence T(n) = Θ(n^p(1+I n))) in the forcing-dominated regime p + 1 ≤ q, the critical regime q = p, and the deep leaf-dominated regime 0 ≤ q < p (established by the smoothing-function argument). The companion module Section_04_7_Akra_Bazzi.Generalized closes the remaining exponent regimes, including p = 0 and p < q < p + 1, under the same PolynomialGrowth predicate. Its public akraBazzi_bigTheta_nonneg theorem is exported by the chapter guide. The predicate requires monotonicity and a positive two-sided monomial sandwich; children are explicit floors, not unrestricted perturbations.

Notation conventions used in this section:

  • aᵢ : the number of subproblems of branch i

  • bᵢ : the size divisor of branch i (a real > 1)

  • p : the Akra–Bazzi root exponent

  • g : the driving (additive) function

namespace CLRSnamespace Chapter04

The Akra–Bazzi hypotheses

A branch (aᵢ, bᵢ) of an Akra–Bazzi recurrence: aᵢ subproblems, each of size n / bᵢ, with aᵢ ≥ 1 and bᵢ > 1.

structure AkraBazziBranch where a : ℕ b : ℝ ha_pos : 0 < a hb_gt_one : 1 < b

An Akra–Bazzi recurrence. branches is the nonempty list of branches, g is the driving function, and T is the solution. The recurrence is stated on exact powers of a common base; the floor/ceiling and polynomial-smoothness refinements of the full CLRS statement are left to the gap note.

structure AkraBazziRecurrence where branches : List AkraBazziBranch g : ℕ → ℝ T : ℕ → ℝ hnonempty : branches ≠ []

The root equation

The characteristic term a / b^p of one branch.

noncomputable def charTerm (a : ℕ) (b : ℝ) (p : ℝ) : ℝ := (a : ℝ) / (b : ℝ) ^ p

The characteristic function Σ_i a_i / b_i^p.

noncomputable def charFun (branches : List (ℕ × ℝ)) (p : ℝ) : ℝ := (branches.map (fun ab => charTerm ab.1 ab.2 p)).sum

The Akra–Bazzi root equation Σ_i a_i / b_i^p = 1.

noncomputable def IsAkraBazziRoot (branches : List (ℕ × ℝ)) (p : ℝ) : Prop := charFun branches p = 1

The real base-power identity b^(log_b a) = a for natural a ≥ 1 and b > 1. This is the bridge from the Akra–Bazzi root equation to the master-theorem exponent.

theorem rpow_realLogExponent (a b : ℕ) (ha : 1 ≤ a) (hb : 1 < b) : (b : ℝ) ^ realLogExponent a b = (a : ℝ) := by have hb_pos : 0 < (b : ℝ) := by exact_mod_cast (lt_trans (by norm_num : (0:ℕ) < 1) hb) have hb_log_pos : 0 < Real.log (b : ℝ) := Real.log_pos (by exact_mod_cast hb) have hb_log_ne : Real.log (b : ℝ) ≠ 0 := ne_of_gt hb_log_pos have ha_pos : 0 < (a : ℝ) := by exact_mod_cast (lt_of_lt_of_le (by norm_num : (0:ℕ) < 1) ha) unfold realLogExponent calc (b : ℝ) ^ (Real.log (a : ℝ) / Real.log (b : ℝ)) = Real.exp (Real.log (b : ℝ) * (Real.log (a : ℝ) / Real.log (b : ℝ))) := by rw [Real.rpow_def_of_pos hb_pos] _ = Real.exp (Real.log (a : ℝ)) := by field_simp [hb_log_ne] _ = (a : ℝ) := Real.exp_log ha_pos

Akra–Bazzi root, single branch. The recurrence T(n) = a T(n/b) + g(n) has root p = log_b a, the master-theorem exponent. This is the Akra–Bazzi root equation a / b^p = 1 for one branch.

theorem akraBazziRoot_single (a b : ℕ) (ha : 1 ≤ a) (hb : 1 < b) : IsAkraBazziRoot [(a, (b : ℝ))] (realLogExponent a b) := by unfold IsAkraBazziRoot charFun charTerm simp [List.sum] rw [rpow_realLogExponent a b ha hb] exact div_self (by exact_mod_cast (show (a : ℕ) ≠ 0 by omega))

The single-branch root is unique: two roots p and q must agree. This is the monotonicity of p ↦ a / b^p in a single branch.

theorem akraBazziRoot_single_unique {a b : ℕ} (ha : 1 ≤ a) (hb : 1 < b) {p q : ℝ} (hp : IsAkraBazziRoot [(a, (b : ℝ))] p) (hq : IsAkraBazziRoot [(a, (b : ℝ))] q) : p = q := by have hb_pos : 0 < (b : ℝ) := by exact_mod_cast (lt_trans (by norm_num : (0:ℕ) < 1) hb) have ha_pos : 0 < (a : ℝ) := by exact_mod_cast (lt_of_lt_of_le (by norm_num : (0:ℕ) < 1) ha) have hbp : (b : ℝ) ^ p = (a : ℝ) := by unfold IsAkraBazziRoot charFun charTerm at hp simp [List.sum] at hp field_simp [ne_of_gt (Real.rpow_pos_of_pos hb_pos p)] at hp exact hp.symm have hbq : (b : ℝ) ^ q = (a : ℝ) := by unfold IsAkraBazziRoot charFun charTerm at hq simp [List.sum] at hq field_simp [ne_of_gt (Real.rpow_pos_of_pos hb_pos q)] at hq exact hq.symm have hlog_eq : p * Real.log (b : ℝ) = q * Real.log (b : ℝ) := by calc p * Real.log (b : ℝ) = Real.log ((b : ℝ) ^ p) := by rw [Real.log_rpow hb_pos] _ = Real.log ((b : ℝ) ^ q) := by rw [hbp, hbq] _ = q * Real.log (b : ℝ) := by rw [Real.log_rpow hb_pos] have hb_log_ne : Real.log (b : ℝ) ≠ 0 := ne_of_gt (Real.log_pos (by exact_mod_cast hb)) exact mul_right_cancel₀ hb_log_ne hlog_eq

The two-branch instance

Akra–Bazzi root, classic instance. The two-branch recurrence T(n) = T(n/3) + T(2n/3) + n has root p = 1, since 3^(-1) + (3/2)^(-1) = 1/3 + 2/3 = 1.

theorem akraBazziRoot_two_thirds_one : IsAkraBazziRoot [(1, (3 : ℝ)), (1, (3 : ℝ) / 2)] 1 := by unfold IsAkraBazziRoot charFun charTerm norm_num [List.sum]

The single-branch corollary

Akra–Bazzi single-branch corollary. For a single branch (a, b) the root is p = log_b a, and its scale n^p is exactly the discrete CLRS.­Chapter04.­realLogScale used by the continuous master theorem (§4.6). Hence the Akra–Bazzi method recovers the master-theorem exponent and Θ(n^(log_b a)) bound for polynomial forcing (through CLRS.­Chapter04.­continuous_master_case1, CLRS.­Chapter04.­continuous_master_case2, and CLRS.­Chapter04.­continuous_master_case3).

theorem akraBazzi_single_branch_corollary (a b : ℕ) (ha : 1 ≤ a) (hb : 1 < b) : IsAkraBazziRoot [(a, (b : ℝ))] (realLogExponent a b) ∧ (∀ n : ℕ, (n : ℝ) ^ realLogExponent a b = realLogScale a b n) := by constructor · exact akraBazziRoot_single a b ha hb · intro n rfl

The multi-branch root: monotonicity, uniqueness, and scale invariance

A branch (aᵢ, bᵢ) is valid when 0 < aᵢ and 1 < bᵢ.

def BranchValid (ab : ℕ × ℝ) : Prop := 0 < ab.1 ∧ 1 < ab.2

Every branch in the list is BranchValid.

def BranchesValid (branches : List (ℕ × ℝ)) : Prop := ∀ ab ∈ branches, BranchValid ab

The characteristic term a / b^p is strictly decreasing in p for a valid branch: raising the exponent p shrinks b^(-p) (since b > 1), hence shrinks the whole term a · b^(-p).

lemma charTerm_lt_of_lt {a : ℕ} {b p q : ℝ} (ha : 0 < a) (hb : 1 < b) (hpq : p < q) : charTerm a b q < charTerm a b p := by unfold charTerm have hb_pos : 0 < b := lt_trans (by norm_num : (0 : ℝ) < 1) hb have hbpq : b ^ p < b ^ q := Real.rpow_lt_rpow_of_exponent_lt hb hpq have hbinv : (b ^ q)⁻¹ < (b ^ p)⁻¹ := inv_strictAntiOn (Real.rpow_pos_of_pos hb_pos p) (Real.rpow_pos_of_pos hb_pos q) hbpq have ha_pos : 0 < (a : ℝ) := by exact_mod_cast ha simpa [div_eq_mul_inv] using (mul_lt_mul_of_pos_left hbinv ha_pos : (a : ℝ) * (b ^ q)⁻¹ < (a : ℝ) * (b ^ p)⁻¹)

The characteristic function Σ aᵢ / bᵢ^p is strictly decreasing in p for a nonempty valid branch list. Every term shrinks, so the sum shrinks.

theorem charFun_lt_of_lt {branches : List (ℕ × ℝ)} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) {p q : ℝ} (hpq : p < q) : charFun branches q < charFun branches p := by rcases branches with _ | ⟨ab, rest⟩ · contradiction · have hvalid_ab : BranchValid ab := hvalid ab (by simp) unfold charFun simp only [List.map_cons, List.sum_cons] have hhead : charTerm ab.1 ab.2 q < charTerm ab.1 ab.2 p := charTerm_lt_of_lt hvalid_ab.1 hvalid_ab.2 hpq have hrest : (rest.map (fun x => charTerm x.1 x.2 q)).sum ≤ (rest.map (fun x => charTerm x.1 x.2 p)).sum := by apply List.sum_le_sum intro x hx have hvalid_x : BranchValid x := hvalid x (by simp [hx]) exact le_of_lt (charTerm_lt_of_lt hvalid_x.1 hvalid_x.2 hpq) -- head + rest_q < head_p + rest_p exact add_lt_add_of_lt_of_le hhead hrest

Akra–Bazzi root uniqueness (multi-branch). The root equation Σ aᵢ / bᵢ^p = 1 has at most one real solution, because charFun is strictly decreasing. This generalizes akraBazziRoot_single_unique from a single branch to any nonempty valid branch list.

theorem akraBazziRoot_unique {branches : List (ℕ × ℝ)} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) {p q : ℝ} (hp : IsAkraBazziRoot branches p) (hq : IsAkraBazziRoot branches q) : p = q := by by_contra hne rcases lt_or_gt_of_ne hne with hpq | hqp · have hlt : charFun branches q < charFun branches p := charFun_lt_of_lt hvalid hnonempty hpq rw [hp, hq] at hlt exact (lt_irrefl _ hlt).elim · have hlt : charFun branches p < charFun branches q := charFun_lt_of_lt hvalid hnonempty hqp rw [hp, hq] at hlt exact (lt_irrefl _ hlt).elim

Akra–Bazzi root is nonnegative. Since charFun 0 = Σ aᵢ ≥ 1 and charFun is strictly decreasing down to 1, the root satisfies p ≥ 0.

theorem akraBazziRoot_nonneg {branches : List (ℕ × ℝ)} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) {p : ℝ} (hp : IsAkraBazziRoot branches p) : 0 ≤ p := by by_contra hpneg have hp_lt : p < 0 := lt_of_not_ge hpneg have hchar : charFun branches 0 < charFun branches p := charFun_lt_of_lt hvalid hnonempty hp_lt have hchar0_ge : 1 ≤ charFun branches 0 := by rcases branches with _ | ⟨ab, rest⟩ · contradiction · have hvalid_ab : BranchValid ab := hvalid ab (by simp) unfold charFun charTerm simp only [List.map_cons, List.sum_cons, Real.rpow_zero, div_one] have hab_ge : 1 ≤ (ab.1 : ℝ) := by exact_mod_cast (Nat.succ_le_iff.mpr hvalid_ab.1) have hrest_nonneg : 0 ≤ (rest.map (fun x : ℕ × ℝ => (x.1 : ℝ))).sum := by apply List.sum_nonneg intro y hy rw [List.mem_map] at hy rcases hy with ⟨x, _hx, rfl⟩ exact Nat.cast_nonneg x.1 linarith rw [hp] at hchar linarith

Akra–Bazzi scale invariance (multi-branch). For a root p, the p-weight of one level of the recursion tree is preserved: Σᵢ aᵢ (n / bᵢ)^p = n^p. This is the fundamental bridge from the root equation Σ aᵢ / bᵢ^p = 1 to the scale n^p that governs every level, and it is the multi-branch generalization of akraBazziRoot_single.

theorem akraBazzi_root_scale_invariance (branches : List (ℕ × ℝ)) (p : ℝ) (hvalid : BranchesValid branches) (hroot : IsAkraBazziRoot branches p) (n : ℕ) : (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p)).sum = (n : ℝ) ^ p := by have hn_nonneg : 0 ≤ (n : ℝ) := by positivity have hmap : branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p) = branches.map (fun ab => (n : ℝ) ^ p * ((ab.1 : ℝ) / ab.2 ^ p)) := by rw [List.map_eq_map_iff] intro ab hab have hb_nonneg : 0 ≤ ab.2 := le_of_lt (lt_trans (by norm_num : (0 : ℝ) < 1) (hvalid ab hab).2) rw [Real.div_rpow hn_nonneg hb_nonneg] ring rw [hmap] rw [List.sum_map_mul_left] change (n : ℝ) ^ p * charFun branches p = (n : ℝ) ^ p rw [hroot] ring

The integral asymptotic form

The Akra–Bazzi integral: the discrete form of ∫₁ⁿ g(u) / u^(p+1) du, summed over u = 1, …, n. This is the sum the recursion tree accumulates.

noncomputable def akraBazziIntegral (p : ℝ) (g : ℕ → ℝ) (n : ℕ) : ℝ := ∑ u ∈ Finset.range n, g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1)

The Akra–Bazzi scale: the discrete form of the textbook n^p (1 + ∫₁ⁿ g(u) / u^(p+1) du).

noncomputable def akraBazziScale (p : ℝ) (g : ℕ → ℝ) (n : ℕ) : ℝ := (n : ℝ) ^ p * (1 + akraBazziIntegral p g n)

The per-branch integral increment at size n: a (n/b)^p (I n - I ⌊n/b⌋) — the amount of scale n^p "lost" by rounding the subproblem size down from n/b to ⌊n/b⌋.

noncomputable def akraBazziIncrement (p : ℝ) (g : ℕ → ℝ) (ab : ℕ × ℝ) (n : ℕ) : ℝ := (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (akraBazziIntegral p g n - akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊))

Polynomial growth (smoothness) of the driving function. The forcing function g is nonnegative, nondecreasing, and sandwiched between two positive monomials of a common exponent q: c n^q ≤ g n ≤ C n^q. This is the discrete, total-function analogue of CLRS's polynomially bounded driving function, and it is the regularity assumption under which the recursion tree compares to the integral scale.

def PolynomialGrowth (g : ℕ → ℝ) (q : ℝ) : Prop := (∀ n : ℕ, 0 ≤ g n) ∧ (∀ {m n : ℕ}, m ≤ n → g m ≤ g n) ∧ ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ (∀ n : ℕ, 1 ≤ n → c * (n : ℝ) ^ q ≤ g n) ∧ (∀ n : ℕ, 1 ≤ n → g n ≤ C * (n : ℝ) ^ q)

The recurrence T(n) = Σᵢ aᵢ T(⌊n/bᵢ⌋) + g(n) with a constant base case. The floor ⌊n/bᵢ⌋ is the perturbation of CLRS §4.7: the argument is rounded down to the nearest integer subproblem size. T is 0 at 0, 1 for 1 ≤ n ≤ n₀, and satisfies the recurrence above the base-case threshold n₀.

def SatisfiesAkraBazzi (branches : List (ℕ × ℝ)) (g T : ℕ → ℝ) (n₀ : ℕ) : Prop := T 0 = 0 ∧ (∀ n, 1 ≤ n → n ≤ n₀ → T n = 1) ∧ (∀ n, n₀ < n → T n = (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum + g n)

Recurrence-to-integral comparison

The floor-perturbed subproblem size is strictly smaller than its parent.

lemma floor_div_lt_self {b : ℝ} (hb : 1 < b) {n : ℕ} (hn : 0 < n) : ⌊(n : ℝ) / b⌋₊ < n := by have hb_pos : 0 < b := lt_trans (by norm_num : (0 : ℝ) < 1) hb have hn_pos : 0 < (n : ℝ) := by exact_mod_cast hn have hdiv_lt : (n : ℝ) / b < (n : ℝ) := by rw [div_lt_iff₀ hb_pos] simpa using (mul_lt_mul_of_pos_left hb hn_pos : (n : ℝ) * 1 < (n : ℝ) * b) have hfl : (⌊(n : ℝ) / b⌋₊ : ℝ) ≤ (n : ℝ) / b := Nat.floor_le (le_of_lt (div_pos hn_pos hb_pos)) exact_mod_cast (lt_of_le_of_lt hfl hdiv_lt)

The Akra–Bazzi integral is nonnegative.

lemma akraBazziIntegral_nonneg {p : ℝ} {g : ℕ → ℝ} (hg : ∀ n, 0 ≤ g n) (n : ℕ) : 0 ≤ akraBazziIntegral p g n := by unfold akraBazziIntegral apply Finset.sum_nonneg intro u _hu exact div_nonneg (hg (u + 1)) (Real.rpow_nonneg (by positivity) (p + 1))

The Akra–Bazzi integral is monotone in its upper limit.

lemma akraBazziIntegral_mono {p : ℝ} {g : ℕ → ℝ} (hg : ∀ n, 0 ≤ g n) {m n : ℕ} (hmn : m ≤ n) : akraBazziIntegral p g m ≤ akraBazziIntegral p g n := by unfold akraBazziIntegral rw [← Nat.add_sub_of_le hmn] rw [Finset.sum_range_add (fun u => g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1)) m (n - m)] exact le_add_of_nonneg_right (Finset.sum_nonneg (by intro x _hx exact div_nonneg (hg (m + x + 1)) (Real.rpow_nonneg (by positivity) (p + 1))))

The integral increment I n - I m is the tail sum over u ∈ (m, n].

lemma akraBazziIntegral_sub {p : ℝ} {g : ℕ → ℝ} {m n : ℕ} (hmn : m ≤ n) : akraBazziIntegral p g n - akraBazziIntegral p g m = ∑ u ∈ Finset.range (n - m), g (m + u + 1) / ((m + u + 1 : ℕ) : ℝ) ^ (p + 1) := by unfold akraBazziIntegral let f : ℕ → ℝ := fun u => g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1) have hsum : ∑ u ∈ Finset.range n, f u = ∑ u ∈ Finset.range m, f u + ∑ u ∈ Finset.range (n - m), f (m + u) := by conv_lhs => rw [← Nat.add_sub_of_le hmn] rw [Finset.sum_range_add f m (n - m)] rw [hsum] rw [add_sub_cancel_left]

The integral is bounded below by a positive constant (the first term).

lemma akraBazziIntegral_lower_const {p q : ℝ} {g : ℕ → ℝ} (hsmooth : PolynomialGrowth g q) : ∃ c : ℝ, 0 < c ∧ ∀ n, 1 ≤ n → c ≤ akraBazziIntegral p g n := by rcases hsmooth with ⟨hgnonneg, _hgmono, c, _C, hcpos, _hCpos, hglower, _hgupper⟩ refine ⟨c, hcpos, ?_⟩ intro n hn unfold akraBazziIntegral have hterm : c ≤ g 1 / (1 : ℝ) ^ (p + 1) := by have hg1 := hglower 1 (by norm_num : 1 ≤ 1) simpa using hg1 have hterm_le_sum : g 1 / (1 : ℝ) ^ (p + 1) ≤ ∑ u ∈ Finset.range n, g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1) := by have h0mem : 0 ∈ Finset.range n := by rw [Finset.mem_range]; exact hn have := Finset.single_le_sum (f := fun u => g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1)) (by intro u _hu; exact div_nonneg (hgnonneg (u + 1)) (Real.rpow_nonneg (by positivity) (p + 1))) h0mem simpa using this exact le_trans hterm hterm_le_sum

The Akra–Bazzi scale is nonnegative at every input.

lemma akraBazziScale_nonneg {p : ℝ} {g : ℕ → ℝ} (Variable name `hp` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hp : 0 ≤ p) (hg : ∀ n, 0 ≤ g n) (n : ℕ) : 0 ≤ akraBazziScale p g n := by unfold akraBazziScale have hn : 0 ≤ (n : ℝ) ^ p := Real.rpow_nonneg (by positivity) p have hI : 0 ≤ akraBazziIntegral p g n := akraBazziIntegral_nonneg hg n positivity

The integral is bounded for q < p: the forcing g ≤ C n^q gives a convergent p-series Σ u^(q-p-1).

lemma akraBazziIntegral_bounded_of_lt {p q : ℝ} {g : ℕ → ℝ} (hsmooth : PolynomialGrowth g q) (hqp : q < p) : ∃ C : ℝ, ∀ n, akraBazziIntegral p g n ≤ C := by rcases hsmooth with ⟨_hgnonneg, _hgmono, _c, Cg, _hcpos, hCpos, _hglower, hgupper⟩ have hδ : 1 < p - q + 1 := by linarith have hsum : Summable (fun v : ℕ => (v : ℝ) ^ (q - p - 1)) := by have h0 : Summable (fun n : ℕ => ((n : ℝ) ^ (p - q + 1))⁻¹) := (Real.summable_nat_rpow_inv (p := p - q + 1)).mpr hδ refine h0.congr ?_ intro n rw [← Real.rpow_neg (by positivity : 0 ≤ (n : ℝ)) (p - q + 1)] congr 1 ring refine ⟨Cg * (∑' v : ℕ, (v : ℝ) ^ (q - p - 1)), ?_⟩ intro n unfold akraBazziIntegral calc (∑ u ∈ Finset.range n, g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1)) ≤ ∑ u ∈ Finset.range n, Cg * ((u + 1 : ℕ) : ℝ) ^ (q - p - 1) := by apply Finset.sum_le_sum intro u _hu have hu1 : 1 ≤ u + 1 := by omega have hg : g (u + 1) ≤ Cg * ((u + 1 : ℕ) : ℝ) ^ q := hgupper (u + 1) hu1 calc g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ Cg * ((u + 1 : ℕ) : ℝ) ^ q / ((u + 1 : ℕ) : ℝ) ^ (p + 1) := div_le_div_of_nonneg_right hg (Real.rpow_nonneg (by positivity) (p + 1)) _ = Cg * (((u + 1 : ℕ) : ℝ) ^ q / ((u + 1 : ℕ) : ℝ) ^ (p + 1)) := by ring _ = Cg * ((u + 1 : ℕ) : ℝ) ^ (q - p - 1) := by rw [show q - p - 1 = q - (p + 1) by ring] rw [Real.rpow_sub (by positivity : 0 < ((u + 1 : ℕ) : ℝ)) q (p + 1)] _ = Cg * ∑ u ∈ Finset.range n, ((u + 1 : ℕ) : ℝ) ^ (q - p - 1) := by rw [Finset.mul_sum] _ ≤ Cg * ∑ v ∈ Finset.range (n + 1), (v : ℝ) ^ (q - p - 1) := by apply mul_le_mul_of_nonneg_left _ hCpos.le rw [Finset.sum_range_succ' (fun v => (v : ℝ) ^ (q - p - 1)) n] exact le_add_of_nonneg_right (by positivity) _ ≤ Cg * (∑' v : ℕ, (v : ℝ) ^ (q - p - 1)) := by exact mul_le_mul_of_nonneg_left (Summable.sum_le_tsum (Finset.range (n + 1)) (by intro v _hv; exact Real.rpow_nonneg (by positivity) (q - p - 1)) hsum) hCpos.le

The upper comparison

The integral tail I n - I m is at least the number of terms times the smallest term.

lemma akraBazziIntegral_tail_lower {p : ℝ} {g : ℕ → ℝ} (hp : 0 ≤ p) (hgnonneg : ∀ n, 0 ≤ g n) (hgmono : ∀ {m n : ℕ}, m ≤ n → g m ≤ g n) {m n : ℕ} (hmn : m ≤ n) : ((n - m : ℕ) : ℝ) * (g m / (n : ℝ) ^ (p + 1)) ≤ akraBazziIntegral p g n - akraBazziIntegral p g m := by rw [akraBazziIntegral_sub hmn] rw [show ((n - m : ℕ) : ℝ) * (g m / (n : ℝ) ^ (p + 1)) = ∑ u ∈ Finset.range (n - m), (g m / (n : ℝ) ^ (p + 1)) by rw [Finset.sum_const, nsmul_eq_mul, Finset.card_range]] apply Finset.sum_le_sum intro u hu have hle_n : m + u + 1 ≤ n := by have hu_lt : u < n - m := by simpa [Finset.mem_range] using hu omega have hge_m : m ≤ m + u + 1 := by omega have hg : g m ≤ g (m + u + 1) := hgmono hge_m have hpow : ((m + u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ (n : ℝ) ^ (p + 1) := Real.rpow_le_rpow (by positivity) (by exact_mod_cast hle_n) (by linarith : 0 ≤ p + 1) have h1 : g m / (n : ℝ) ^ (p + 1) ≤ g (m + u + 1) / (n : ℝ) ^ (p + 1) := div_le_div_of_nonneg_right hg (Real.rpow_nonneg (by positivity) (p + 1)) exact le_trans h1 (div_le_div_of_nonneg_left (hgnonneg (m + u + 1)) (Real.rpow_pos_of_pos (by positivity) (p + 1)) hpow)

The single-branch integral increment a (n/b)^p (I n - I ⌊n/b⌋) dominates g n by a positive factor eventually. This is the analytic core of the upper-bound substitution proof.

lemma akraBazzi_increment_lower {a : ℕ} {b p q : ℝ} {g : ℕ → ℝ} (ha : 0 < a) (hb : 1 < b) (hp : 0 ≤ p) (hq : 0 ≤ q) (hsmooth : PolynomialGrowth g q) : ∃ ε : ℝ, 0 < ε ∧ ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → (a : ℝ) * ((n : ℝ) / b) ^ p * (akraBazziIntegral p g n - akraBazziIntegral p g (⌊(n : ℝ) / b⌋₊)) ≥ ε * g n := by rcases hsmooth with ⟨hgnonneg, hgmono, c, C, hcpos, hCpos, hglower, hgupper⟩ have hb_pos : 0 < b := lt_trans (by norm_num : (0 : ℝ) < 1) hb have ha_pos : 0 < (a : ℝ) := by exact_mod_cast ha let ε : ℝ := (a : ℝ) * (1 - 1 / b) * b ^ (-p) * c * (2 * b) ^ (-q) / C have hsub_pos : 0 < 1 - 1 / b := by have h1 : (1 : ℝ) / b < 1 := (div_lt_one hb_pos).mpr hb linarith have hε_pos : 0 < ε := by dsimp [ε] positivity let n₁ : ℕ := Nat.ceil (2 * b) + 1 refine ⟨ε, hε_pos, n₁, ?_⟩ intro n hn have hn_2b : 2 * b ≤ (n : ℝ) := by have hceil : 2 * b ≤ (Nat.ceil (2 * b) : ℝ) := Nat.le_ceil (2 * b) have hn₁' : (Nat.ceil (2 * b) + 1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn have hceil1 : (Nat.ceil (2 * b) : ℝ) ≤ (Nat.ceil (2 * b) + 1 : ℝ) := by norm_num linarith have hn_pos_nat : 0 < n := by have h2b : 0 < 2 * b := by positivity exact_mod_cast (lt_of_lt_of_le h2b hn_2b) have hn_pos : 0 < (n : ℝ) := by exact_mod_cast hn_pos_nat let m : ℕ := ⌊(n : ℝ) / b⌋₊ have hm_lt_n : m < n := floor_div_lt_self hb hn_pos_nat have hm_le : (m : ℝ) ≤ (n : ℝ) / b := Nat.floor_le (le_of_lt (div_pos hn_pos hb_pos)) have hm_ge_half : (n : ℝ) / (2 * b) ≤ (m : ℝ) := by have hfl : (n : ℝ) / b - 1 ≤ (m : ℝ) := by have hlt : (n : ℝ) / b < (m : ℝ) + 1 := Nat.lt_floor_add_one ((n : ℝ) / b) linarith have h2 : (n : ℝ) / (2 * b) ≤ (n : ℝ) / b - 1 := by field_simp [hb_pos] linarith exact le_trans h2 hfl have hm_ge_one : 1 ≤ m := by have hm1 : (1 : ℝ) ≤ (m : ℝ) := by have h : (1 : ℝ) ≤ (n : ℝ) / (2 * b) := by rw [le_div_iff₀ (by positivity : 0 < (2 * b : ℝ))] simpa using hn_2b exact le_trans h hm_ge_half exact_mod_cast hm1 have hg_m : c * (2 * b) ^ (-q) / C * g n ≤ g m := by have hm_q : c * (m : ℝ) ^ q ≤ g m := hglower m hm_ge_one have hgn : g n ≤ C * (n : ℝ) ^ q := hgupper n hn_pos_nat have hm_nq : c * (2 * b) ^ (-q) * (n : ℝ) ^ q ≤ g m := by have hmn : (n : ℝ) / (2 * b) ≤ (m : ℝ) := hm_ge_half have hpow : ((n : ℝ) / (2 * b)) ^ q ≤ (m : ℝ) ^ q := Real.rpow_le_rpow (by positivity) hmn hq have h1 : c * ((n : ℝ) / (2 * b)) ^ q ≤ g m := le_trans (mul_le_mul_of_nonneg_left hpow hcpos.le) hm_q have h2 : ((n : ℝ) / (2 * b)) ^ q = (n : ℝ) ^ q * (2 * b) ^ (-q) := by rw [Real.div_rpow (by positivity) (by positivity : 0 ≤ 2 * b)] rw [Real.rpow_neg (by positivity : 0 ≤ 2 * b) q] rw [div_eq_mul_inv] rw [h2] at h1 simpa [mul_comm, mul_left_comm, mul_assoc] using h1 have h3 : c * (2 * b) ^ (-q) / C * g n ≤ c * (2 * b) ^ (-q) * (n : ℝ) ^ q := by have hgn_div : g n / C ≤ (n : ℝ) ^ q := by rw [div_le_iff₀ hCpos] simpa [mul_comm] using hgn have hnn : c * (2 * b) ^ (-q) * (g n / C) ≤ c * (2 * b) ^ (-q) * (n : ℝ) ^ q := mul_le_mul_of_nonneg_left hgn_div (mul_nonneg hcpos.le (Real.rpow_nonneg (by positivity) (-q))) have hrewrite : c * (2 * b) ^ (-q) / C * g n = c * (2 * b) ^ (-q) * (g n / C) := by field_simp [ne_of_gt hCpos] rwa [hrewrite] exact le_trans h3 hm_nq have htail : ((n - m : ℕ) : ℝ) * (g m / (n : ℝ) ^ (p + 1)) ≤ akraBazziIntegral p g n - akraBazziIntegral p g m := akraBazziIntegral_tail_lower hp hgnonneg hgmono (le_of_lt hm_lt_n) have hn_card : (n : ℝ) * (1 - 1 / b) ≤ (n - m : ℕ) := by have hsub : (n : ℝ) - (n : ℝ) / b ≤ (n - m : ℕ) := by rw [Nat.cast_sub (le_of_lt hm_lt_n)] linarith have h1 : (n : ℝ) * (1 - 1 / b) = (n : ℝ) - (n : ℝ) / b := by ring rw [h1] exact hsub have hid : ((n : ℝ) / b) ^ p * (n : ℝ) / (n : ℝ) ^ (p + 1) = b ^ (-p) := by rw [Real.div_rpow (by positivity) hb_pos.le] rw [Real.rpow_add hn_pos p 1, Real.rpow_one] field_simp [ne_of_gt (Real.rpow_pos_of_pos hn_pos p), ne_of_gt (Real.rpow_pos_of_pos hb_pos p)] rw [Real.rpow_neg hb_pos.le p] exact (mul_inv_cancel₀ (ne_of_gt (Real.rpow_pos_of_pos hb_pos p))).symm have halg : (a : ℝ) * ((n : ℝ) / b) ^ p * (((n : ℝ) * (1 - 1 / b)) * (g m / (n : ℝ) ^ (p + 1))) = (a : ℝ) * (1 - 1 / b) * b ^ (-p) * (g m) := by rw [div_eq_mul_inv] calc (a : ℝ) * ((n : ℝ) / b) ^ p * (((n : ℝ) * (1 - 1 / b)) * (g m * ((n : ℝ) ^ (p + 1))⁻¹)) = (a : ℝ) * (1 - 1 / b) * (g m) * (((n : ℝ) / b) ^ p * (n : ℝ) * ((n : ℝ) ^ (p + 1))⁻¹) := by ring _ = (a : ℝ) * (1 - 1 / b) * (g m) * b ^ (-p) := by rw [show ((n : ℝ) / b) ^ p * (n : ℝ) * ((n : ℝ) ^ (p + 1))⁻¹ = b ^ (-p) by simpa [div_eq_mul_inv] using hid] _ = (a : ℝ) * (1 - 1 / b) * b ^ (-p) * (g m) := by ring calc (a : ℝ) * ((n : ℝ) / b) ^ p * (akraBazziIntegral p g n - akraBazziIntegral p g m) ≥ (a : ℝ) * ((n : ℝ) / b) ^ p * (((n - m : ℕ) : ℝ) * (g m / (n : ℝ) ^ (p + 1))) := mul_le_mul_of_nonneg_left htail (mul_nonneg ha_pos.le (Real.rpow_nonneg (by positivity) p)) _ ≥ (a : ℝ) * ((n : ℝ) / b) ^ p * (((n : ℝ) * (1 - 1 / b)) * (g m / (n : ℝ) ^ (p + 1))) := mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_right (by exact_mod_cast hn_card) (div_nonneg (hgnonneg m) (Real.rpow_nonneg (by positivity) (p + 1)))) (mul_nonneg ha_pos.le (Real.rpow_nonneg (by positivity) p)) _ = (a : ℝ) * (1 - 1 / b) * b ^ (-p) * (g m) := halg _ ≥ (a : ℝ) * (1 - 1 / b) * b ^ (-p) * (c * (2 * b) ^ (-q) / C * g n) := mul_le_mul_of_nonneg_left hg_m (mul_nonneg (mul_nonneg ha_pos.le (le_of_lt hsub_pos)) (Real.rpow_nonneg hb_pos.le (-p))) _ = ε * g n := by dsimp [ε]; ring

The increment upper bound (smallness)

The integral tail I n - I m is at most the number of terms times the largest term g n / m^(p+1). This is the companion of akraBazziIntegral_tail_lower: the tail is squeezed between the smallest and largest term counts.

lemma akraBazziIntegral_tail_upper {p : ℝ} {g : ℕ → ℝ} (hp : 0 ≤ p) (hgnonneg : ∀ n, 0 ≤ g n) (hgmono : ∀ {m n : ℕ}, m ≤ n → g m ≤ g n) {m n : ℕ} (hmn : m ≤ n) (hm_pos : 0 < m) : akraBazziIntegral p g n - akraBazziIntegral p g m ≤ ((n - m : ℕ) : ℝ) * g n / (m : ℝ) ^ (p + 1) := by rw [akraBazziIntegral_sub hmn] have hm_pos' : 0 < (m : ℝ) := by exact_mod_cast hm_pos have hle_each : ∀ u ∈ Finset.range (n - m), g (m + u + 1) / ((m + u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ g n / (m : ℝ) ^ (p + 1) := by intro u hu have hu_lt : u < n - m := by simpa [Finset.mem_range] using hu have hle_n : m + u + 1 ≤ n := by omega have hge_m : m ≤ m + u + 1 := by omega have hg : g (m + u + 1) ≤ g n := hgmono hle_n have hpow : (m : ℝ) ^ (p + 1) ≤ ((m + u + 1 : ℕ) : ℝ) ^ (p + 1) := Real.rpow_le_rpow (by positivity) (by exact_mod_cast hge_m) (by linarith : 0 ≤ p + 1) have hdiv : g (m + u + 1) / ((m + u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ g n / ((m + u + 1 : ℕ) : ℝ) ^ (p + 1) := div_le_div_of_nonneg_right hg (Real.rpow_nonneg (by positivity) (p + 1)) exact le_trans hdiv (div_le_div_of_nonneg_left (hgnonneg n) (Real.rpow_pos_of_pos (by positivity) (p + 1)) hpow) calc ∑ u ∈ Finset.range (n - m), g (m + u + 1) / ((m + u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ ∑ u ∈ Finset.range (n - m), g n / (m : ℝ) ^ (p + 1) := by exact Finset.sum_le_sum (fun u hu => hle_each u hu) _ = ((n - m : ℕ) : ℝ) * (g n / (m : ℝ) ^ (p + 1)) := by rw [Finset.sum_const, nsmul_eq_mul, Finset.card_range] _ = ((n - m : ℕ) : ℝ) * g n / (m : ℝ) ^ (p + 1) := by ring

A helper: foldr max 0 l is at least every element of l.

lemma List_foldr_max_ge_mem {l : List ℕ} {x : ℕ} (hx : x ∈ l) : x ≤ l.foldr max 0 := by induction l with | nil => simp at hx | cons h t ih => rw [List.foldr_cons] simp only [List.mem_cons] at hx rcases hx with rfl | hx' · exact le_max_left _ _ · exact le_trans (ih hx') (le_max_right _ _)

The single-branch integral increment a (n/b)^p (I n - I ⌊n/b⌋) is at most a constant multiple of g n. This is the analytic core of the lower-bound substitution proof: the increment lost to the floor rounding is comparable to (not larger than) the forcing term g n.

lemma akraBazzi_increment_upper_single {a : ℕ} {b p : ℝ} {g : ℕ → ℝ} (Variable name `ha` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`ha : 0 < a) (hb : 1 < b) (hp : 0 ≤ p) (hgnonneg : ∀ n, 0 ≤ g n) (hgmono : ∀ {m n : ℕ}, m ≤ n → g m ≤ g n) : ∀ n : ℕ, Nat.ceil (2 * b) + 1 ≤ n → akraBazziIncrement p g (a, b) n ≤ (a : ℝ) * 2 ^ (p + 1) * b * g n := by have hb_pos : 0 < b := lt_trans (by norm_num : (0 : ℝ) < 1) hb intro n hn have hn_2b : 2 * b ≤ (n : ℝ) := by have hceil : 2 * b ≤ (Nat.ceil (2 * b) : ℝ) := Nat.le_ceil (2 * b) have hn₁' : (Nat.ceil (2 * b) + 1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn have hceil1 : (Nat.ceil (2 * b) : ℝ) ≤ (Nat.ceil (2 * b) + 1 : ℝ) := by norm_num linarith have hn_pos_nat : 0 < n := by have h2b : 0 < 2 * b := by positivity exact_mod_cast (lt_of_lt_of_le h2b hn_2b) have hn_pos : 0 < (n : ℝ) := by exact_mod_cast hn_pos_nat let m : ℕ := ⌊(n : ℝ) / b⌋₊ have hm_lt_n : m < n := floor_div_lt_self hb hn_pos_nat have hm_le_n : m ≤ n := le_of_lt hm_lt_n have hm_ge_half : (n : ℝ) / (2 * b) ≤ (m : ℝ) := by have hfl : (n : ℝ) / b - 1 ≤ (m : ℝ) := by have hlt : (n : ℝ) / b < (m : ℝ) + 1 := Nat.lt_floor_add_one ((n : ℝ) / b) linarith have h2 : (n : ℝ) / (2 * b) ≤ (n : ℝ) / b - 1 := by field_simp [hb_pos] linarith exact le_trans h2 hfl have hm_ge_one_nat : 1 ≤ m := by have hm1 : (1 : ℝ) ≤ (m : ℝ) := by have h : (1 : ℝ) ≤ (n : ℝ) / (2 * b) := by rw [le_div_iff₀ (by positivity : 0 < (2 * b : ℝ))] simpa using hn_2b exact le_trans h hm_ge_half exact_mod_cast hm1 have hm_pos : 0 < m := lt_of_lt_of_le (by norm_num : (0 : ℕ) < 1) hm_ge_one_nat have hm_pos' : 0 < (m : ℝ) := by exact_mod_cast hm_pos have htail : akraBazziIntegral p g n - akraBazziIntegral p g m ≤ ((n - m : ℕ) : ℝ) * g n / (m : ℝ) ^ (p + 1) := akraBazziIntegral_tail_upper hp hgnonneg hgmono hm_le_n hm_pos have hnm : ((n - m : ℕ) : ℝ) ≤ (n : ℝ) := by have : (n - m : ℕ) ≤ n := Nat.sub_le n m exact_mod_cast this have hm_pow_le : ((n : ℝ) / (2 * b)) ^ (p + 1) ≤ (m : ℝ) ^ (p + 1) := Real.rpow_le_rpow (by positivity) hm_ge_half (by linarith : 0 ≤ p + 1) have htail2 : ((n - m : ℕ) : ℝ) * g n / (m : ℝ) ^ (p + 1) ≤ (2 * b) ^ (p + 1) * g n / (n : ℝ) ^ p := by have hnum : ((n - m : ℕ) : ℝ) * g n ≤ (n : ℝ) * g n := mul_le_mul_of_nonneg_right hnm (hgnonneg n) have hdiv_le : (n : ℝ) * g n / (m : ℝ) ^ (p + 1) ≤ (n : ℝ) * g n / ((n : ℝ) / (2 * b)) ^ (p + 1) := div_le_div_of_nonneg_left (mul_nonneg hn_pos.le (hgnonneg n)) (Real.rpow_pos_of_pos (div_pos hn_pos (by positivity : 0 < 2 * b)) (p + 1)) hm_pow_le have hid : (n : ℝ) * g n / ((n : ℝ) / (2 * b)) ^ (p + 1) = (2 * b) ^ (p + 1) * g n / (n : ℝ) ^ p := by rw [Real.div_rpow (by positivity) (by positivity : 0 ≤ 2 * b)] rw [div_div_eq_mul_div] have h2 : (n : ℝ) / (n : ℝ) ^ (p + 1) = 1 / (n : ℝ) ^ p := by rw [show (n : ℝ) ^ (p + 1) = (n : ℝ) ^ p * (n : ℝ) by rw [Real.rpow_add hn_pos p 1, Real.rpow_one]] field_simp [ne_of_gt hn_pos, ne_of_gt (Real.rpow_pos_of_pos hn_pos p)] calc (n : ℝ) * g n * (2 * b) ^ (p + 1) / (n : ℝ) ^ (p + 1) = ((n : ℝ) / (n : ℝ) ^ (p + 1)) * g n * (2 * b) ^ (p + 1) := by ring _ = (1 / (n : ℝ) ^ p) * g n * (2 * b) ^ (p + 1) := by rw [h2] _ = (2 * b) ^ (p + 1) * g n / (n : ℝ) ^ p := by ring calc ((n - m : ℕ) : ℝ) * g n / (m : ℝ) ^ (p + 1) ≤ (n : ℝ) * g n / (m : ℝ) ^ (p + 1) := div_le_div_of_nonneg_right hnum (Real.rpow_nonneg (by positivity) (p + 1)) _ ≤ (n : ℝ) * g n / ((n : ℝ) / (2 * b)) ^ (p + 1) := hdiv_le _ = (2 * b) ^ (p + 1) * g n / (n : ℝ) ^ p := hid have halg : (a : ℝ) * ((n : ℝ) / b) ^ p * ((2 * b) ^ (p + 1) * g n / (n : ℝ) ^ p) = (a : ℝ) * 2 ^ (p + 1) * b * g n := by have hquot : ((n : ℝ) / b) ^ p / (n : ℝ) ^ p = b ^ (-p) := by rw [Real.div_rpow (by positivity) hb_pos.le] rw [Real.rpow_neg hb_pos.le p] rw [show (n : ℝ) ^ p / b ^ p / (n : ℝ) ^ p = (b ^ p)⁻¹ by rw [show (n : ℝ) ^ p / b ^ p / (n : ℝ) ^ p = (n : ℝ) ^ p * (b ^ p)⁻¹ * ((n : ℝ) ^ p)⁻¹ by rw [div_eq_mul_inv] rfl] calc (n : ℝ) ^ p * (b ^ p)⁻¹ * ((n : ℝ) ^ p)⁻¹ = (b ^ p)⁻¹ * ((n : ℝ) ^ p * ((n : ℝ) ^ p)⁻¹) := by ring _ = (b ^ p)⁻¹ * 1 := by rw [mul_inv_cancel₀ (ne_of_gt (Real.rpow_pos_of_pos hn_pos p))] _ = (b ^ p)⁻¹ := by ring] have hmul : b ^ (-p) * (2 * b) ^ (p + 1) = 2 ^ (p + 1) * b := by rw [Real.mul_rpow (by norm_num : 0 ≤ (2 : ℝ)) hb_pos.le] have h1 : b ^ (-p) * b ^ (p + 1) = b := by rw [← Real.rpow_add hb_pos (-p) (p + 1)] rw [show -p + (p + 1) = 1 by ring] rw [Real.rpow_one] calc b ^ (-p) * (2 ^ (p + 1) * b ^ (p + 1)) = 2 ^ (p + 1) * (b ^ (-p) * b ^ (p + 1)) := by ring _ = 2 ^ (p + 1) * b := by rw [h1] calc (a : ℝ) * ((n : ℝ) / b) ^ p * ((2 * b) ^ (p + 1) * g n / (n : ℝ) ^ p) = (a : ℝ) * (((n : ℝ) / b) ^ p / (n : ℝ) ^ p) * (2 * b) ^ (p + 1) * g n := by ring _ = (a : ℝ) * b ^ (-p) * (2 * b) ^ (p + 1) * g n := by rw [hquot] _ = (a : ℝ) * (2 ^ (p + 1) * b) * g n := by rw [show (a : ℝ) * b ^ (-p) * (2 * b) ^ (p + 1) * g n = (a : ℝ) * (b ^ (-p) * (2 * b) ^ (p + 1)) * g n by ring] rw [hmul] _ = (a : ℝ) * 2 ^ (p + 1) * b * g n := by ring calc akraBazziIncrement p g (a, b) n = (a : ℝ) * ((n : ℝ) / b) ^ p * (akraBazziIntegral p g n - akraBazziIntegral p g m) := by rfl _ ≤ (a : ℝ) * ((n : ℝ) / b) ^ p * (((n - m : ℕ) : ℝ) * g n / (m : ℝ) ^ (p + 1)) := mul_le_mul_of_nonneg_left htail (mul_nonneg (Nat.cast_nonneg a) (Real.rpow_nonneg (by positivity) p)) _ ≤ (a : ℝ) * ((n : ℝ) / b) ^ p * ((2 * b) ^ (p + 1) * g n / (n : ℝ) ^ p) := mul_le_mul_of_nonneg_left htail2 (mul_nonneg (Nat.cast_nonneg a) (Real.rpow_nonneg (by positivity) p)) _ = (a : ℝ) * 2 ^ (p + 1) * b * g n := halg

The multi-branch increment Σᵢ aᵢ (n/bᵢ)^p (I n - I ⌊n/bᵢ⌋) is at most a constant multiple of g n. Each branch is bounded by akraBazzi_increment_upper_single, and the terms are summed.

lemma akraBazzi_increment_upper {branches : List (ℕ × ℝ)} {p : ℝ} {g : ℕ → ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hp : 0 ≤ p) (hgnonneg : ∀ n, 0 ≤ g n) (hgmono : ∀ {m n : ℕ}, m ≤ n → g m ≤ g n) : ∃ K : ℝ, 0 < K ∧ ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → (branches.map (fun ab => akraBazziIncrement p g ab n)).sum ≤ K * g n := by let K : ℝ := (2 : ℝ) ^ (p + 1) * (branches.map (fun ab => (ab.1 : ℝ) * ab.2)).sum have hK_pos : 0 < K := by dsimp [K] have h2 : 0 < (2 : ℝ) ^ (p + 1) := Real.rpow_pos_of_pos (by norm_num : 0 < (2 : ℝ)) (p + 1) have hsum : 0 < (branches.map (fun ab => (ab.1 : ℝ) * ab.2)).sum := by rcases branches with _ | ⟨ab, rest⟩ · contradiction · have hvalid_ab : BranchValid ab := hvalid ab (by simp) have hab : 0 < (ab.1 : ℝ) * ab.2 := by have ha : 0 < (ab.1 : ℝ) := by exact_mod_cast hvalid_ab.1 have hb : 0 < ab.2 := lt_trans (by norm_num : (0 : ℝ) < 1) hvalid_ab.2 exact mul_pos ha hb have hrest_nonneg : 0 ≤ (rest.map (fun x => (x.1 : ℝ) * x.2)).sum := by apply List.sum_nonneg intro y hy rw [List.mem_map] at hy rcases hy with ⟨x, _hx, rfl⟩ have hvalid_x : BranchValid x := hvalid x (by simp [_hx]) exact mul_nonneg (Nat.cast_nonneg x.1) (le_of_lt (lt_trans (by norm_num : (0 : ℝ) < 1) hvalid_x.2)) exact lt_of_lt_of_le hab (by rw [List.map_cons, List.sum_cons] exact le_add_of_nonneg_right hrest_nonneg) exact mul_pos h2 hsum let n₁ : ℕ := (branches.map (fun ab => Nat.ceil (2 * ab.2) + 1)).foldr max 0 refine ⟨K, hK_pos, n₁, ?_⟩ intro n hn have hsum_le : (branches.map (fun ab => akraBazziIncrement p g ab n)).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * 2 ^ (p + 1) * ab.2 * g n)).sum := by apply List.sum_le_sum intro ab hab have hvalid_ab : BranchValid ab := hvalid ab hab have hx_threshold : Nat.ceil (2 * ab.2) + 1 ≤ n := by have hx_in_fold : Nat.ceil (2 * ab.2) + 1 ≤ n₁ := by dsimp [n₁] exact List_foldr_max_ge_mem (by rw [List.mem_map] refine ⟨ab, hab, rfl⟩) exact le_trans hx_in_fold hn exact akraBazzi_increment_upper_single (a := ab.1) (b := ab.2) (p := p) (g := g) hvalid_ab.1 hvalid_ab.2 hp hgnonneg hgmono n hx_threshold calc (branches.map (fun ab => akraBazziIncrement p g ab n)).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * 2 ^ (p + 1) * ab.2 * g n)).sum := hsum_le _ = ((2 : ℝ) ^ (p + 1) * (branches.map (fun ab => (ab.1 : ℝ) * ab.2)).sum) * g n := by rw [show (branches.map (fun ab => (ab.1 : ℝ) * 2 ^ (p + 1) * ab.2 * g n)).sum = ((2 : ℝ) ^ (p + 1) * (branches.map (fun ab => (ab.1 : ℝ) * ab.2)).sum) * g n by calc (branches.map (fun ab => (ab.1 : ℝ) * 2 ^ (p + 1) * ab.2 * g n)).sum = (branches.map (fun ab => (2 : ℝ) ^ (p + 1) * g n * ((ab.1 : ℝ) * ab.2))).sum := by exact congrArg List.sum (List.map_congr_left (by intro ab _hab; ring)) _ = (2 : ℝ) ^ (p + 1) * g n * (branches.map (fun ab => (ab.1 : ℝ) * ab.2)).sum := by rw [List.sum_map_mul_left branches (fun ab => (ab.1 : ℝ) * ab.2) ((2 : ℝ) ^ (p + 1) * g n)] _ = ((2 : ℝ) ^ (p + 1) * (branches.map (fun ab => (ab.1 : ℝ) * ab.2)).sum) * g n := by ring] _ = K * g n := by rfl

The multi-branch increment Σᵢ aᵢ (n/bᵢ)^p (I n - I ⌊n/bᵢ⌋) is at least a positive constant multiple of g n. One branch is bounded below by akraBazzi_increment_lower; the other branches contribute nonnegatively.

lemma akraBazzi_increment_lower_multi {branches : List (ℕ × ℝ)} {p q : ℝ} {g : ℕ → ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hp : 0 ≤ p) (hq : 0 ≤ q) (hsmooth : PolynomialGrowth g q) : ∃ ε : ℝ, 0 < ε ∧ ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ε * g n ≤ (branches.map (fun ab => akraBazziIncrement p g ab n)).sum := by have hgnonneg : ∀ n, 0 ≤ g n := hsmooth.1 rcases branches with _ | ⟨ab, rest⟩ · contradiction · have hvalid_ab : BranchValid ab := hvalid ab (by simp) rcases akraBazzi_increment_lower (a := ab.1) (b := ab.2) (p := p) (q := q) (g := g) hvalid_ab.1 hvalid_ab.2 hp hq hsmooth with ⟨ε, hε, n₁, hn₁⟩ refine ⟨ε, hε, n₁, ?_⟩ intro n hn have hrest_nonneg : 0 ≤ (rest.map (fun x : ℕ × ℝ => akraBazziIncrement p g x n)).sum := by apply List.sum_nonneg intro x hx rw [List.mem_map] at hx rcases hx with ⟨y, _hy, rfl⟩ have hvalid_y : BranchValid y := hvalid y (by simp [_hy]) have hdiff_nonneg : 0 ≤ akraBazziIntegral p g n - akraBazziIntegral p g (⌊(n : ℝ) / y.2⌋₊) := by have hle : ⌊(n : ℝ) / y.2⌋₊ ≤ n := by have hy2 : 1 < y.2 := hvalid_y.2 have hpos2 : 0 < y.2 := lt_trans (by norm_num : (0 : ℝ) < 1) hy2 have hfl : (⌊(n : ℝ) / y.2⌋₊ : ℝ) ≤ (n : ℝ) / y.2 := Nat.floor_le (div_nonneg (Nat.cast_nonneg n) (le_of_lt hpos2)) have hdiv_le : (n : ℝ) / y.2 ≤ (n : ℝ) := by rw [div_le_iff₀ hpos2] simpa [one_mul, mul_comm] using mul_le_mul_of_nonneg_right (le_of_lt hy2) (Nat.cast_nonneg n) exact_mod_cast (le_trans hfl hdiv_le) exact sub_nonneg.mpr (akraBazziIntegral_mono hgnonneg hle) exact mul_nonneg (mul_nonneg (Nat.cast_nonneg y.1) (Real.rpow_nonneg (div_nonneg (Nat.cast_nonneg n) (le_of_lt (lt_trans (by norm_num : (0 : ℝ) < 1) hvalid_y.2))) p)) hdiff_nonneg calc ε * g n ≤ akraBazziIncrement p g ab n := hn₁ n hn _ ≤ akraBazziIncrement p g ab n + (rest.map (fun x : ℕ × ℝ => akraBazziIncrement p g x n)).sum := le_add_of_nonneg_right hrest_nonneg _ = ((ab :: rest).map (fun x : ℕ × ℝ => akraBazziIncrement p g x n)).sum := by rfl

The recurrence-to-integral comparison

The Akra–Bazzi scale is at least 1 whenever n ≥ 1.

lemma akraBazzi_scale_ge_one {p : ℝ} {g : ℕ → ℝ} (hp : 0 ≤ p) (hgnonneg : ∀ n, 0 ≤ g n) {n : ℕ} (hn : 1 ≤ n) : 1 ≤ akraBazziScale p g n := by unfold akraBazziScale have hn' : 1 ≤ (n : ℝ) := by exact_mod_cast hn have hnp : 1 ≤ (n : ℝ) ^ p := by calc 1 = (1 : ℝ) ^ p := by rw [Real.one_rpow] _ ≤ (n : ℝ) ^ p := Real.rpow_le_rpow (by norm_num : 0 ≤ (1 : ℝ)) hn' hp have hI : 0 ≤ akraBazziIntegral p g n := akraBazziIntegral_nonneg hgnonneg n have h1I : 1 ≤ 1 + akraBazziIntegral p g n := by linarith exact one_le_mul_of_one_le_of_one_le hnp h1I

The decomposition of the scale at one level of the recursion tree: the weighted sum of the children's scales Σᵢ aᵢ (n/bᵢ)^p (1 + I ⌊n/bᵢ⌋) equals the scale n^p (1 + I n) minus the total increment Σᵢ aᵢ (n/bᵢ)^p (I n - I ⌊n/bᵢ⌋).

lemma akraBazzi_scale_decomp (branches : List (ℕ × ℝ)) (p : ℝ) (g : ℕ → ℝ) (n : ℕ) (hvalid : BranchesValid branches) (hroot : IsAkraBazziRoot branches p) : (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum = akraBazziScale p g n - (branches.map (fun ab => akraBazziIncrement p g ab n)).sum := by unfold akraBazziScale akraBazziIncrement have hsum : (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum + (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (akraBazziIntegral p g n - akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum = (n : ℝ) ^ p * (1 + akraBazziIntegral p g n) := by rw [← List.sum_map_add] have hmap : (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)) + (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (akraBazziIntegral p g n - akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum = (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g n))).sum := by exact congrArg List.sum (List.map_congr_left (by intro ab _hab; ring)) rw [hmap] rw [List.sum_map_mul_right branches (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p) (1 + akraBazziIntegral p g n)] rw [akraBazzi_root_scale_invariance branches p hvalid hroot n] linarith

A solution of an Akra–Bazzi recurrence is nonnegative.

try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false` lemma akraBazzi_T_nonneg {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} (hvalid : BranchesValid branches) (hgnonneg : ∀ n, 0 ≤ g n) (hsat : SatisfiesAkraBazzi branches g T n₀) : ∀ n, 0 ≤ T n := by intro n induction n using Nat.strong_induction_on with | h n ih => by_cases hn0 : n = 0 · subst n try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [hsat.1] · have hn_pos : 0 < n := Nat.pos_of_ne_zero hn0 by_cases hle : n ≤ n₀ · rw [hsat.2.1 n (Nat.succ_le_iff.mpr hn_pos) hle] norm_num · have hn₀n : n₀ < n := lt_of_not_ge hle rw [hsat.2.2 n hn₀n] exact add_nonneg (by apply List.sum_nonneg intro x hx rw [List.mem_map] at hx rcases hx with ⟨ab, hab, rfl⟩ have hvalid_ab : BranchValid ab := hvalid ab hab have hlt : ⌊(n : ℝ) / ab.2⌋₊ < n := floor_div_lt_self hvalid_ab.2 hn_pos exact mul_nonneg (Nat.cast_nonneg ab.1) (ih (⌊(n : ℝ) / ab.2⌋₊) hlt)) (hgnonneg n)

Akra–Bazzi upper bound. The solution T of the multi-branch recurrence is O(n^p (1 + I n)) where I n = Σ_{u≤n} g(u)/u^(p+1). This is the upper half of the recurrence-to-integral comparison: the forcing g is absorbed by the per-level increment akraBazziIncrement, which is bounded below by akraBazzi_increment_lower_multi.

theorem akraBazzi_upper_bound_nonneg {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p q : ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches p) (hp : 0 ≤ p) (hq : 0 ≤ q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigO T (akraBazziScale p g) := by have hgnonneg : ∀ n, 0 ≤ g n := hsmooth.1 rcases akraBazzi_increment_lower_multi hvalid hnonempty hp hq hsmooth with ⟨ε, hε, n₁, hinc⟩ have hT_nonneg : ∀ n, 0 ≤ T n := akraBazzi_T_nonneg hvalid hgnonneg hsat let Tsum : ℝ := ∑ m ∈ Finset.range (n₁ + 1), T m let C : ℝ := 1 + ε⁻¹ + Tsum have hC_pos : 0 < C := by dsimp [C] have hε_inv : 0 < ε⁻¹ := inv_pos.mpr hε have hTsum : 0 ≤ Tsum := by dsimp [Tsum] exact Finset.sum_nonneg (by intro m _hm; exact hT_nonneg m) positivity have hC_ge_one : 1 ≤ C := by dsimp [C] have hε_inv : 0 ≤ ε⁻¹ := le_of_lt (inv_pos.mpr hε) have hTsum : 0 ≤ Tsum := by dsimp [Tsum] exact Finset.sum_nonneg (by intro m _hm; exact hT_nonneg m) linarith have hC_ge_inv : ε⁻¹ ≤ C := by dsimp [C] have hTsum : 0 ≤ Tsum := by dsimp [Tsum] exact Finset.sum_nonneg (by intro m _hm; exact hT_nonneg m) linarith have hmain : ∀ n, T n ≤ C * akraBazziScale p g n := by intro n induction n using Nat.strong_induction_on with | h n ih => by_cases hn0 : n = 0 · subst n rw [hsat.1] exact mul_nonneg hC_pos.le (akraBazziScale_nonneg hp hgnonneg 0) · have hn_pos : 0 < n := Nat.pos_of_ne_zero hn0 have hn_pos' : 1 ≤ n := Nat.succ_le_iff.mpr hn_pos by_cases hle : n ≤ n₀ · -- base case have hF1 : 1 ≤ akraBazziScale p g n := akraBazzi_scale_ge_one hp hgnonneg hn_pos' calc T n = 1 := hsat.2.1 n hn_pos' hle _ ≤ C := hC_ge_one _ ≤ C * akraBazziScale p g n := by calc C = C * 1 := by rw [mul_one] _ ≤ C * akraBazziScale p g n := mul_le_mul_of_nonneg_left hF1 hC_pos.le · have hn₀n : n₀ < n := lt_of_not_ge hle by_cases hsmall : n ≤ n₁ · -- finite initial range: T n ≤ C, and 1 ≤ F n have hTn_le : T n ≤ C := by have hsum_dom : T n ≤ Tsum := by dsimp [Tsum] have hn_mem : n ∈ Finset.range (n₁ + 1) := by rw [Finset.mem_range] exact Nat.lt_succ_of_le hsmall exact Finset.single_le_sum (by intro m _hm; exact hT_nonneg m) hn_mem have hε_inv_nonneg : 0 ≤ ε⁻¹ := le_of_lt (inv_pos.mpr hε) dsimp [C] linarith have hF1 : 1 ≤ akraBazziScale p g n := akraBazzi_scale_ge_one hp hgnonneg hn_pos' calc T n ≤ C := hTn_le _ ≤ C * akraBazziScale p g n := by calc C = C * 1 := by rw [mul_one] _ ≤ C * akraBazziScale p g n := mul_le_mul_of_nonneg_left hF1 hC_pos.le · -- main induction step have hn₁n : n₁ ≤ n := le_of_not_ge hsmall have hIH : ∀ ab ∈ branches, T (⌊(n : ℝ) / ab.2⌋₊) ≤ C * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊) := by intro ab hab have hvalid_ab : BranchValid ab := hvalid ab hab have hlt : ⌊(n : ℝ) / ab.2⌋₊ < n := floor_div_lt_self hvalid_ab.2 hn_pos exact ih (⌊(n : ℝ) / ab.2⌋₊) hlt have hsum_le : (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum ≤ C * (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by calc (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * (C * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by apply List.sum_le_sum intro ab hab exact mul_le_mul_of_nonneg_left (hIH ab hab) (Nat.cast_nonneg ab.1) _ = C * (branches.map (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊))).sum := by rw [show (branches.map (fun ab => (ab.1 : ℝ) * (C * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)))).sum = C * (branches.map (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊))).sum by calc (branches.map (fun ab => (ab.1 : ℝ) * (C * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)))).sum = (branches.map (fun ab => C * ((ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by exact congrArg List.sum (List.map_congr_left (by intro ab _hab; ring)) _ = C * (branches.map (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊))).sum := by rw [List.sum_map_mul_left branches (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)) C]] _ ≤ C * (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by apply mul_le_mul_of_nonneg_left _ hC_pos.le apply List.sum_le_sum intro ab hab have hvalid_ab : BranchValid ab := hvalid ab hab unfold akraBazziScale have hfloor : (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ≤ (n : ℝ) / ab.2 := Nat.floor_le (le_of_lt (div_pos (by exact_mod_cast hn_pos) (lt_trans (by norm_num : (0 : ℝ) < 1) hvalid_ab.2))) have hpow : (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p ≤ ((n : ℝ) / ab.2) ^ p := Real.rpow_le_rpow (by positivity) hfloor hp have hnonneg : 0 ≤ 1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊) := add_nonneg (by norm_num) (akraBazziIntegral_nonneg hgnonneg _) simpa [mul_assoc] using mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_right hpow hnonneg) (Nat.cast_nonneg ab.1) have hdecomp := akraBazzi_scale_decomp branches p g n hvalid hroot have hinc_bound : ε * g n ≤ (branches.map (fun ab => akraBazziIncrement p g ab n)).sum := hinc n hn₁n calc T n = (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum + g n := hsat.2.2 n hn₀n _ ≤ C * (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum + g n := add_le_add_left hsum_le (g n) _ = C * (akraBazziScale p g n - (branches.map (fun ab => akraBazziIncrement p g ab n)).sum) + g n := by rw [hdecomp] _ = C * akraBazziScale p g n - C * (branches.map (fun ab => akraBazziIncrement p g ab n)).sum + g n := by ring _ ≤ C * akraBazziScale p g n - C * (ε * g n) + g n := by exact add_le_add_left (sub_le_sub_left (mul_le_mul_of_nonneg_left hinc_bound hC_pos.le) (C * akraBazziScale p g n)) (g n) _ = C * akraBazziScale p g n - (C * ε - 1) * g n := by ring _ ≤ C * akraBazziScale p g n := by have hCeps : 1 ≤ C * ε := by have : ε⁻¹ * ε ≤ C * ε := mul_le_mul_of_nonneg_right hC_ge_inv (le_of_lt hε) have hεε : ε⁻¹ * ε = 1 := inv_mul_cancel₀ (ne_of_gt hε) simpa [hεε] using this have hnonneg_g : 0 ≤ g n := hgnonneg n have hCeps1 : 0 ≤ C * ε - 1 := by linarith have hsub : (C * ε - 1) * g n ≥ 0 := mul_nonneg hCeps1 hnonneg_g linarith rw [Chapter03.isBigO_iff] refine ⟨C, hC_pos, 0, ?_⟩ intro n hn rw [abs_of_nonneg (hT_nonneg n)] rw [abs_of_nonneg (akraBazziScale_nonneg hp hgnonneg n)] exact hmain n

The positive-root specialization of the upper recurrence comparison.

theorem akraBazzi_upper_bound {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p q : ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches p) (hp : 0 < p) (hq : 0 ≤ q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigO T (akraBazziScale p g) := akraBazzi_upper_bound_nonneg hvalid hnonempty hroot hp.le hq hsmooth hsat

The lower comparison

Above the base threshold, a solution of an Akra–Bazzi recurrence is at least the forcing term: the recursion tree only adds nonnegative work on top of g n.

lemma akraBazzi_T_ge_g {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} (hvalid : BranchesValid branches) (hgnonneg : ∀ n, 0 ≤ g n) (hsat : SatisfiesAkraBazzi branches g T n₀) : ∀ n, n₀ < n → g n ≤ T n := by intro n hn₀n have hT_nonneg : ∀ n, 0 ≤ T n := akraBazzi_T_nonneg hvalid hgnonneg hsat rw [hsat.2.2 n hn₀n] have hsum_nonneg : 0 ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum := by apply List.sum_nonneg intro x hx rw [List.mem_map] at hx rcases hx with ⟨ab, hab, rfl⟩ exact mul_nonneg (Nat.cast_nonneg ab.1) (hT_nonneg _) linarith

For p + 1 ≤ q, the integral is bounded by a polynomial C n^(q-p).

lemma akraBazzi_integral_le_poly {p q : ℝ} {g : ℕ → ℝ} (hsmooth : PolynomialGrowth g q) (hpq : p + 1 ≤ q) : ∃ C : ℝ, 0 < C ∧ ∀ n, akraBazziIntegral p g n ≤ C * (n : ℝ) ^ (q - p) := by rcases hsmooth with ⟨_hgnonneg, _hgmono, _c, Cg, _hcpos, hCpos, _hglower, hgupper⟩ have hqmp : 0 ≤ q - p - 1 := by linarith refine ⟨Cg, hCpos, ?_⟩ intro n unfold akraBazziIntegral calc (∑ u ∈ Finset.range n, g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1)) ≤ ∑ u ∈ Finset.range n, Cg * ((u + 1 : ℕ) : ℝ) ^ (q - p - 1) := by apply Finset.sum_le_sum intro u _hu have hu1 : 1 ≤ u + 1 := by omega have hg : g (u + 1) ≤ Cg * ((u + 1 : ℕ) : ℝ) ^ q := hgupper (u + 1) hu1 calc g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ Cg * ((u + 1 : ℕ) : ℝ) ^ q / ((u + 1 : ℕ) : ℝ) ^ (p + 1) := div_le_div_of_nonneg_right hg (Real.rpow_nonneg (by positivity) (p + 1)) _ = Cg * ((u + 1 : ℕ) : ℝ) ^ (q - p - 1) := by rw [show q - p - 1 = q - (p + 1) by ring] rw [show Cg * ((u + 1 : ℕ) : ℝ) ^ q / ((u + 1 : ℕ) : ℝ) ^ (p + 1) = Cg * (((u + 1 : ℕ) : ℝ) ^ q / ((u + 1 : ℕ) : ℝ) ^ (p + 1)) by ring] rw [show ((u + 1 : ℕ) : ℝ) ^ q / ((u + 1 : ℕ) : ℝ) ^ (p + 1) = ((u + 1 : ℕ) : ℝ) ^ (q - (p + 1)) by exact (Real.rpow_sub (by exact_mod_cast (Nat.succ_pos u) : 0 < ((u+1:ℕ):ℝ)) q (p + 1)).symm] _ ≤ ∑ u ∈ Finset.range n, Cg * (n : ℝ) ^ (q - p - 1) := by apply Finset.sum_le_sum intro u _hu have hu_le : (u + 1 : ℕ) ≤ n := by have : u < n := by simpa [Finset.mem_range] using _hu omega exact mul_le_mul_of_nonneg_left (Real.rpow_le_rpow (by positivity) (by exact_mod_cast hu_le) hqmp) hCpos.le _ = Cg * (n : ℝ) ^ (q - p - 1) * (n : ℕ) := by rw [Finset.sum_const, nsmul_eq_mul, Finset.card_range] ring _ = Cg * (n : ℝ) ^ (q - p) := by have hpow : (n : ℝ) ^ (q - p - 1) * (n : ℝ) = (n : ℝ) ^ (q - p) := by rw [show (n : ℝ) ^ (q - p) = (n : ℝ) ^ ((q - p - 1) + 1) by congr 1; ring] rw [Real.rpow_add' (Nat.cast_nonneg n) (by linarith [hpq] : (q - p - 1) + 1 ≠ 0)] rw [Real.rpow_one] rw [show Cg * (n : ℝ) ^ (q - p - 1) * (n : ℕ) = Cg * ((n : ℝ) ^ (q - p - 1) * (n : ℝ)) by ring] rw [hpow]

For 2 ≤ x and 0 < p, the power drop from x to ⌊x⌋₊ is O(x^(p-1)): a one-step mean-value bound on the monotone power map.

lemma rpow_sub_floor_le_of_two_le {p : ℝ} (hp : 0 < p) {x : ℝ} (hx2 : 2 ≤ x) : x ^ p - (⌊x⌋₊ : ℝ) ^ p ≤ 2 * (1 + p) * x ^ (p - 1) := by have hx0 : 0 < x := lt_of_lt_of_le (by norm_num) hx2 by_cases hx_int : (⌊x⌋₊ : ℝ) = x · rw [hx_int] have hnonneg : 0 ≤ 2 * (1 + p) * x ^ (p - 1) := by positivity linarith · have hfloor_le : (⌊x⌋₊ : ℝ) ≤ x := Nat.floor_le hx0.le have hfloor_ge : x - 1 ≤ (⌊x⌋₊ : ℝ) := by have h := Nat.lt_floor_add_one x linarith have hfloor_ge_half : x / 2 ≤ (⌊x⌋₊ : ℝ) := by have h1 : x / 2 ≤ x - 1 := by linarith exact le_trans h1 hfloor_ge have hfloor_ge_one : 1 ≤ (⌊x⌋₊ : ℝ) := by have h1 : (1 : ℝ) ≤ x / 2 := by linarith exact le_trans h1 hfloor_ge_half have hlt : (⌊x⌋₊ : ℝ) < x := lt_of_le_of_ne hfloor_le hx_int have hmvt : ∃ c ∈ Set.Ioo (⌊x⌋₊ : ℝ) x, deriv (fun z : ℝ => z ^ p) c = (x ^ p - (⌊x⌋₊ : ℝ) ^ p) / (x - (⌊x⌋₊ : ℝ)) := by refine exists_deriv_eq_slope (fun z : ℝ => z ^ p) hlt ?_ ?_ · exact (Real.continuous_rpow_const hp.le).continuousOn.mono (Set.subset_univ _) · intro z hz rw [Set.mem_Ioo] at hz have hz_pos : 0 < z := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_trans hfloor_ge_one (le_of_lt hz.1)) exact (Real.differentiableAt_rpow_const_of_ne p (ne_of_gt hz_pos)).differentiableWithinAt rcases hmvt with ⟨c, hcIoo, hc⟩ have hc_pos : 0 < c := by rw [Set.mem_Ioo] at hcIoo exact lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_trans hfloor_ge_one (le_of_lt hcIoo.1)) have hc_le_x : c ≤ x := by rw [Set.mem_Ioo] at hcIoo exact le_of_lt hcIoo.2 have hc_ge_half : x / 2 ≤ c := by rw [Set.mem_Ioo] at hcIoo exact le_trans hfloor_ge_half (le_of_lt hcIoo.1) have hden_pos : 0 < x - (⌊x⌋₊ : ℝ) := sub_pos.mpr hlt have hden_le_one : x - (⌊x⌋₊ : ℝ) ≤ 1 := by have h := Nat.lt_floor_add_one x linarith have hmain : x ^ p - (⌊x⌋₊ : ℝ) ^ p = p * c ^ (p - 1) * (x - (⌊x⌋₊ : ℝ)) := by rw [Real.deriv_rpow_const] at hc rw [eq_div_iff (ne_of_gt hden_pos)] at hc exact hc.symm have hcp : c ^ (p - 1) ≤ 2 * x ^ (p - 1) := by by_cases hp1 : 1 ≤ p · have h : 0 ≤ p - 1 := sub_nonneg.mpr hp1 calc c ^ (p - 1) ≤ x ^ (p - 1) := Real.rpow_le_rpow hc_pos.le hc_le_x h _ ≤ 2 * x ^ (p - 1) := by have hx_p1_nonneg : 0 ≤ x ^ (p - 1) := Real.rpow_nonneg hx0.le (p - 1) nlinarith · have hp_lt_one : p < 1 := lt_of_not_ge hp1 have hneg : p - 1 < 0 := sub_neg.mpr hp_lt_one have hx_half_pos : 0 < x / 2 := by positivity have hhalf : (x / 2) ^ (p - 1) = (2 : ℝ) ^ (1 - p) * x ^ (p - 1) := by rw [Real.div_rpow hx0.le (by norm_num : 0 ≤ (2 : ℝ))] rw [div_eq_mul_inv] rw [← Real.rpow_neg (by norm_num : 0 ≤ (2 : ℝ)) (p - 1)] rw [show -(p - 1) = 1 - p by ring] ring calc c ^ (p - 1) ≤ (x / 2) ^ (p - 1) := Real.rpow_le_rpow_of_nonpos hx_half_pos hc_ge_half (le_of_lt hneg) _ = (2 : ℝ) ^ (1 - p) * x ^ (p - 1) := hhalf _ ≤ 2 * x ^ (p - 1) := by have h2 : (2 : ℝ) ^ (1 - p) ≤ 2 := by have hsub : 1 - p ≤ 1 := by nlinarith have hle : (2 : ℝ) ^ (1 - p) ≤ (2 : ℝ) ^ (1 : ℝ) := Real.rpow_le_rpow_of_exponent_le (by norm_num : (1 : ℝ) ≤ 2) hsub rw [Real.rpow_one] at hle exact hle exact mul_le_mul_of_nonneg_right h2 (Real.rpow_nonneg hx0.le (p - 1)) calc x ^ p - (⌊x⌋₊ : ℝ) ^ p = p * c ^ (p - 1) * (x - (⌊x⌋₊ : ℝ)) := hmain _ ≤ p * c ^ (p - 1) * 1 := by have hnonneg : 0 ≤ p * c ^ (p - 1) := mul_nonneg hp.le (Real.rpow_nonneg hc_pos.le (p - 1)) exact mul_le_mul_of_nonneg_left hden_le_one hnonneg _ = p * c ^ (p - 1) := by ring _ ≤ p * (2 * x ^ (p - 1)) := mul_le_mul_of_nonneg_left hcp hp.le _ = 2 * p * x ^ (p - 1) := by ring _ ≤ 2 * (1 + p) * x ^ (p - 1) := by have hx_p1_nonneg : 0 ≤ x ^ (p - 1) := Real.rpow_nonneg hx0.le (p - 1) nlinarith

The summed power floor loss Σᵢ aᵢ ((n/bᵢ)^p - ⌊n/bᵢ⌋^p) is at most a constant multiple of n^(p-1). This is the sub-leading loss of rounding the subproblem size down; it is what the driving term absorbs in the critical regime.

lemma akraBazzi_power_floor_loss {branches : List (ℕ × ℝ)} {p : ℝ} (hvalid : BranchesValid branches) (hp : 0 < p) : ∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, ∀ n, n₀ ≤ n → (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p))).sum ≤ C * (n : ℝ) ^ (p - 1) := by let C : ℝ := (branches.map (fun ab => (ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p)))).sum + 1 have hC_pos : 0 < C := by dsimp [C] have hsum_nonneg : 0 ≤ (branches.map (fun ab => (ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p)))).sum := by apply List.sum_nonneg intro x hx rw [List.mem_map] at hx rcases hx with ⟨ab, hab, rfl⟩ have hvalid_ab : BranchValid ab := hvalid ab hab have hb_pos : 0 < ab.2 := lt_trans (by norm_num : (0 : ℝ) < 1) hvalid_ab.2 exact mul_nonneg (Nat.cast_nonneg ab.1) (by positivity) linarith let n₀ : ℕ := (branches.map (fun ab => Nat.ceil (2 * ab.2) + 1)).foldr max 0 refine ⟨C, hC_pos, n₀, ?_⟩ intro n hn have hsum_le : (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p))).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p) * (n : ℝ) ^ (p - 1)))).sum := by apply List.sum_le_sum intro ab hab have hvalid_ab : BranchValid ab := hvalid ab hab have hb_pos : 0 < ab.2 := lt_trans (by norm_num : (0 : ℝ) < 1) hvalid_ab.2 have hx_threshold : Nat.ceil (2 * ab.2) + 1 ≤ n := by have hx_in_fold : Nat.ceil (2 * ab.2) + 1 ≤ n₀ := by dsimp [n₀] exact List_foldr_max_ge_mem (by rw [List.mem_map] exact ⟨ab, hab, rfl⟩) exact le_trans hx_in_fold hn have hn_2b : 2 * ab.2 ≤ (n : ℝ) := by have hceil : 2 * ab.2 ≤ (Nat.ceil (2 * ab.2) : ℝ) := Nat.le_ceil (2 * ab.2) have hn' : (Nat.ceil (2 * ab.2) + 1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hx_threshold have hceil1 : (Nat.ceil (2 * ab.2) : ℝ) ≤ (Nat.ceil (2 * ab.2) + 1 : ℝ) := by norm_num linarith have hn_b : 2 ≤ (n : ℝ) / ab.2 := by rw [le_div_iff₀ hb_pos] simpa [mul_comm] using hn_2b have hfloor := rpow_sub_floor_le_of_two_le hp hn_b have hpow : ((n : ℝ) / ab.2) ^ (p - 1) = ab.2 ^ (1 - p) * (n : ℝ) ^ (p - 1) := by rw [Real.div_rpow (Nat.cast_nonneg n) hb_pos.le] rw [div_eq_mul_inv] rw [← Real.rpow_neg hb_pos.le (p - 1)] rw [show -(p - 1) = 1 - p by ring] ring have hnonneg_a : 0 ≤ (ab.1 : ℝ) := Nat.cast_nonneg ab.1 calc (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) ≤ (ab.1 : ℝ) * (2 * (1 + p) * ((n : ℝ) / ab.2) ^ (p - 1)) := mul_le_mul_of_nonneg_left hfloor hnonneg_a _ = (ab.1 : ℝ) * (2 * (1 + p) * (ab.2 ^ (1 - p) * (n : ℝ) ^ (p - 1))) := by rw [hpow] _ = (ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p) * (n : ℝ) ^ (p - 1)) := by ring calc (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p))).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p) * (n : ℝ) ^ (p - 1)))).sum := hsum_le _ = (branches.map (fun ab => (ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p)))).sum * (n : ℝ) ^ (p - 1) := by rw [show (branches.map (fun ab => (ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p) * (n : ℝ) ^ (p - 1)))).sum = (branches.map (fun ab => ((ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p))) * (n : ℝ) ^ (p - 1))).sum by exact congrArg List.sum (List.map_congr_left (by intro ab _hab; ring))] rw [List.sum_map_mul_right branches (fun ab => (ab.1 : ℝ) * (2 * (1 + p) * ab.2 ^ (1 - p))) ((n : ℝ) ^ (p - 1))] _ ≤ C * (n : ℝ) ^ (p - 1) := by have hpow_nonneg : 0 ≤ (n : ℝ) ^ (p - 1) := Real.rpow_nonneg (Nat.cast_nonneg n) (p - 1) dsimp [C] nlinarith

The Akra–Bazzi scale factor 1 + I n is at most a constant multiple of n when the driving function has polynomial growth of exponent p > 0.

lemma akraBazzi_scale_factor_le_linear {p : ℝ} {g : ℕ → ℝ} (Variable name `hp` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hp : 0 < p) (C : ℝ) (hC : 0 < C) (hgupper : ∀ n, 1 ≤ n → g n ≤ C * (n : ℝ) ^ p) : ∃ C' : ℝ, 0 < C' ∧ ∀ n, 1 ≤ n → 1 + akraBazziIntegral p g n ≤ C' * (n : ℝ) := by refine ⟨C + 1, by positivity, ?_⟩ intro n hn have hI : akraBazziIntegral p g n ≤ C * (n : ℝ) := by unfold akraBazziIntegral calc (∑ u ∈ Finset.range n, g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1)) ≤ ∑ u ∈ Finset.range n, C := by apply Finset.sum_le_sum intro u _hu have hu1 : 1 ≤ u + 1 := by omega have hg : g (u + 1) ≤ C * ((u + 1 : ℕ) : ℝ) ^ p := hgupper (u + 1) hu1 calc g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ C * ((u + 1 : ℕ) : ℝ) ^ p / ((u + 1 : ℕ) : ℝ) ^ (p + 1) := div_le_div_of_nonneg_right hg (Real.rpow_nonneg (by positivity) (p + 1)) _ ≤ C := by have hu1' : 1 ≤ ((u + 1 : ℕ) : ℝ) := by exact_mod_cast hu1 have hratio : ((u + 1 : ℕ) : ℝ) ^ p / ((u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ 1 := by rw [← Real.rpow_sub (by positivity : 0 < ((u + 1 : ℕ) : ℝ)) p (p + 1)] rw [show p - (p + 1) = -1 by ring] exact Real.rpow_le_one_of_one_le_of_nonpos hu1' (by norm_num : (-1 : ℝ) ≤ 0) calc C * ((u + 1 : ℕ) : ℝ) ^ p / ((u + 1 : ℕ) : ℝ) ^ (p + 1) = C * (((u + 1 : ℕ) : ℝ) ^ p / ((u + 1 : ℕ) : ℝ) ^ (p + 1)) := by ring _ ≤ C * 1 := mul_le_mul_of_nonneg_left hratio hC.le _ = C := by ring _ = C * (n : ℝ) := by rw [Finset.sum_const, nsmul_eq_mul, Finset.card_range] ring have h1I : 1 + akraBazziIntegral p g n ≤ (C + 1) * (n : ℝ) := by have hn' : 1 ≤ (n : ℝ) := by exact_mod_cast hn nlinarith [hI, hn'] exact h1I

Akra–Bazzi lower bound (forcing-dominated regime). When the driving exponent q strictly exceeds the root p by at least one (so p + 1 ≤ q), the forcing g dominates the recursion tree: T(n) = Ω(n^q), while the scale n^p (1 + I n) = O(n^q), giving T(n) = Ω(n^p (1 + I n)).

theorem akraBazzi_lower_bound {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p q : ℝ} (hvalid : BranchesValid branches) (Variable name `hnonempty` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hnonempty : branches ≠ []) (_hroot : IsAkraBazziRoot branches p) (hp : 0 < p) (hpq : p + 1 ≤ q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigOmega T (akraBazziScale p g) := by have hgnonneg : ∀ n, 0 ≤ g n := hsmooth.1 rcases hsmooth.2.2 with ⟨c₀, _C, hc₀pos, _hCpos, hglower, _hgupper⟩ rcases akraBazzi_integral_le_poly hsmooth hpq with ⟨Ci, _hCipos, hCi⟩ have hT_nonneg : ∀ n, 0 ≤ T n := akraBazzi_T_nonneg hvalid hgnonneg hsat have hT_ge_g : ∀ n, n₀ < n → g n ≤ T n := akraBazzi_T_ge_g hvalid hgnonneg hsat let c : ℝ := c₀ / (1 + Ci) have hc_pos : 0 < c := div_pos hc₀pos (by positivity) rw [Chapter03.isBigOmega_iff] refine ⟨c, hc_pos, n₀ + 1, ?_⟩ intro n hn have hn₀n : n₀ < n := by omega have hn1 : 1 ≤ n := by omega have hg_lower : c₀ * (n : ℝ) ^ q ≤ g n := hglower n hn1 have hF_le : akraBazziScale p g n ≤ (1 + Ci) * (n : ℝ) ^ q := by unfold akraBazziScale have hI : akraBazziIntegral p g n ≤ Ci * (n : ℝ) ^ (q - p) := hCi n have hnp : (n : ℝ) ^ p ≤ (n : ℝ) ^ q := by have hn' : 1 ≤ (n : ℝ) := by exact_mod_cast hn1 exact Real.rpow_le_rpow_of_exponent_le hn' (by linarith [hpq] : p ≤ q) calc (n : ℝ) ^ p * (1 + akraBazziIntegral p g n) ≤ (n : ℝ) ^ p * (1 + Ci * (n : ℝ) ^ (q - p)) := mul_le_mul_of_nonneg_left (by linarith) (Real.rpow_nonneg (by positivity) p) _ = (n : ℝ) ^ p + Ci * ((n : ℝ) ^ p * (n : ℝ) ^ (q - p)) := by ring _ = (n : ℝ) ^ p + Ci * (n : ℝ) ^ q := by have hn_pos : 0 < (n : ℝ) := by exact_mod_cast (lt_of_lt_of_le (by norm_num : (0:ℕ)<1) hn1) rw [show (n : ℝ) ^ p * (n : ℝ) ^ (q - p) = (n : ℝ) ^ q by rw [← Real.rpow_add hn_pos p (q - p)] congr 1; ring] _ ≤ (n : ℝ) ^ q + Ci * (n : ℝ) ^ q := by nlinarith [hnp] _ = (1 + Ci) * (n : ℝ) ^ q := by ring rw [abs_of_nonneg (akraBazziScale_nonneg hp.le hgnonneg n)] rw [abs_of_nonneg (hT_nonneg n)] calc c * akraBazziScale p g n ≤ c * ((1 + Ci) * (n : ℝ) ^ q) := mul_le_mul_of_nonneg_left hF_le hc_pos.le _ = c₀ * (n : ℝ) ^ q := by dsimp [c] field_simp [ne_of_gt (by positivity : 0 < 1 + Ci)] _ ≤ g n := hg_lower _ ≤ T n := hT_ge_g n hn₀n

The scale at the floored subproblem sizes decomposes as the scale minus the increment minus the power floor loss: Σᵢ aᵢ (⌊n/bᵢ⌋)^p (1 + I ⌊n/bᵢ⌋) equals n^p (1 + I n) minus the increment akraBazziIncrement and minus the power rounding loss. This is the lower-bound counterpart of akraBazzi_scale_decomp.

lemma akraBazzi_scale_floor_decomp (branches : List (ℕ × ℝ)) (p : ℝ) (g : ℕ → ℝ) (n : ℕ) (hvalid : BranchesValid branches) (hroot : IsAkraBazziRoot branches p) : (branches.map (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊))).sum = akraBazziScale p g n - (branches.map (fun ab => akraBazziIncrement p g ab n)).sum - (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by unfold akraBazziScale have hsplit : (branches.map (fun ab => (ab.1 : ℝ) * ((⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊))))).sum + (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum = (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by rw [← List.sum_map_add] exact congrArg List.sum (List.map_congr_left (by intro ab _hab; ring)) have hsplit' : (branches.map (fun ab => (ab.1 : ℝ) * ((⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊))))).sum = (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum - (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by linarith rw [hsplit'] rw [akraBazzi_scale_decomp branches p g n hvalid hroot] unfold akraBazziScale akraBazziIncrement ring

Akra–Bazzi lower bound (critical regime). When the driving exponent q equals the root p, the solution is T(n) = Ω(n^p (1 + I n)). This completes the critical case of the lower comparison: the power floor loss is sub-leading, absorbed by the driving term g n together with the increment bound akraBazzi_increment_upper.

theorem akraBazzi_lower_bound_critical {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p : ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches p) (hp : 0 < p) (hsmooth : PolynomialGrowth g p) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigOmega T (akraBazziScale p g) := by have hgnonneg : ∀ n, 0 ≤ g n := hsmooth.1 have hgmono : ∀ {m n : ℕ}, m ≤ n → g m ≤ g n := hsmooth.2.1 rcases hsmooth.2.2 with ⟨c₀, C₀, hc₀pos, hC₀pos, hglower, hgupper⟩ rcases akraBazzi_increment_upper hvalid hnonempty hp.le hgnonneg hgmono with ⟨K, hKpos, n₁, hinc⟩ rcases akraBazzi_power_floor_loss hvalid hp with ⟨Cpl, hCplpos, n₂, hpl⟩ rcases akraBazzi_scale_factor_le_linear hp C₀ hC₀pos hgupper with ⟨Cint, hCintpos, hInt⟩ let M : ℝ := Cpl * Cint / c₀ have hMpos : 0 < M := by dsimp [M]; positivity let N₀ : ℕ := max n₀ (max n₁ n₂) + 1 have hEloss : ∀ n, N₀ ≤ n → (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum ≤ M * g n := by intro n hn have hn₂ : n₂ ≤ n := le_trans (Nat.le_max_right n₁ n₂) (by omega) have hn_pos : 1 ≤ n := by omega have hI_bound : 1 + akraBazziIntegral p g n ≤ Cint * (n : ℝ) := hInt n hn_pos have hpln : (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p))).sum ≤ Cpl * (n : ℝ) ^ (p - 1) := hpl n hn₂ have hD_sum_nonneg : 0 ≤ (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p))).sum := by apply List.sum_nonneg intro x hx rw [List.mem_map] at hx rcases hx with ⟨ab, hab, rfl⟩ have hvalid_ab : BranchValid ab := hvalid ab hab have hb_pos : 0 < ab.2 := lt_trans (by norm_num : (0 : ℝ) < 1) hvalid_ab.2 have hfl : (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ≤ (n : ℝ) / ab.2 := Nat.floor_le (div_nonneg (Nat.cast_nonneg n) (le_of_lt hb_pos)) have hpow_nonneg : 0 ≤ ((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p := sub_nonneg.mpr (Real.rpow_le_rpow (by positivity) hfl hp.le) exact mul_nonneg (Nat.cast_nonneg ab.1) hpow_nonneg have hCint_nonneg : 0 ≤ Cint * (n : ℝ) := mul_nonneg (le_of_lt hCintpos) (Nat.cast_nonneg n) have hnp : (n : ℝ) * (n : ℝ) ^ (p - 1) = (n : ℝ) ^ p := by have hn_pos_real : 0 < (n : ℝ) := by exact_mod_cast (lt_of_lt_of_le (by norm_num : (0 : ℕ) < 1) hn_pos) calc (n : ℝ) * (n : ℝ) ^ (p - 1) = (n : ℝ) ^ (p - 1) * (n : ℝ) := by ring _ = (n : ℝ) ^ ((p - 1) + 1) := (Real.rpow_add_one (ne_of_gt hn_pos_real) (p - 1)).symm _ = (n : ℝ) ^ p := by rw [show (p - 1) + 1 = p by ring] have hsum_le : (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g n))).sum := by apply List.sum_le_sum intro ab hab have hvalid_ab : BranchValid ab := hvalid ab hab have hb_pos : 0 < ab.2 := lt_trans (by norm_num : (0 : ℝ) < 1) hvalid_ab.2 have hfl : (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ≤ (n : ℝ) / ab.2 := Nat.floor_le (div_nonneg (Nat.cast_nonneg n) (le_of_lt hb_pos)) have hfloor_le_nat : ⌊(n : ℝ) / ab.2⌋₊ ≤ n := le_of_lt (floor_div_lt_self hvalid_ab.2 (Nat.succ_le_iff.mp hn_pos)) have hI_mono : akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊) ≤ akraBazziIntegral p g n := akraBazziIntegral_mono hgnonneg hfloor_le_nat have hpow_nonneg : 0 ≤ ((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p := sub_nonneg.mpr (Real.rpow_le_rpow (by positivity) hfl hp.le) have hnonneg_a : 0 ≤ (ab.1 : ℝ) := Nat.cast_nonneg ab.1 exact mul_le_mul_of_nonneg_left (add_le_add_right hI_mono 1) (mul_nonneg hnonneg_a hpow_nonneg) calc (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g n))).sum := hsum_le _ = (1 + akraBazziIntegral p g n) * (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p))).sum := by rw [List.sum_map_mul_right branches (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p)) (1 + akraBazziIntegral p g n)] ring _ ≤ (Cint * (n : ℝ)) * (Cpl * (n : ℝ) ^ (p - 1)) := by exact mul_le_mul hI_bound hpln hD_sum_nonneg hCint_nonneg _ = Cpl * Cint * (n : ℝ) * (n : ℝ) ^ (p - 1) := by ring _ = Cpl * Cint * (n : ℝ) ^ p := by rw [show Cpl * Cint * (n : ℝ) * (n : ℝ) ^ (p - 1) = Cpl * Cint * ((n : ℝ) * (n : ℝ) ^ (p - 1)) by ring] rw [hnp] _ ≤ M * g n := by have hg_lower : c₀ * (n : ℝ) ^ p ≤ g n := hglower n hn_pos have hfac : 0 ≤ Cpl * Cint / c₀ := le_of_lt (by positivity) have h2 := mul_le_mul_of_nonneg_left hg_lower hfac have h3 : (Cpl * Cint / c₀) * (c₀ * (n : ℝ) ^ p) = Cpl * Cint * (n : ℝ) ^ p := by field_simp [ne_of_gt hc₀pos] dsimp [M] rwa [h3] at h2 have hT_nonneg : ∀ n, 0 ≤ T n := akraBazzi_T_nonneg hvalid hgnonneg hsat let Smax : ℝ := ∑ m ∈ Finset.range (N₀ + 1), akraBazziScale p g m have hSmax_pos : 0 < Smax := by dsimp [Smax] have h1mem : 1 ∈ Finset.range (N₀ + 1) := by rw [Finset.mem_range]; omega have h1_scale : 0 < akraBazziScale p g 1 := by unfold akraBazziScale have h1p : 0 < (1 : ℝ) ^ p := Real.rpow_pos_of_pos (by norm_num : 0 < (1 : ℝ)) p have h1I : 0 ≤ akraBazziIntegral p g 1 := akraBazziIntegral_nonneg hgnonneg 1 positivity exact Finset.sum_pos' (by intro m _hm; exact akraBazziScale_nonneg hp.le hgnonneg m) ⟨1, h1mem, h1_scale⟩ let Tmin : ℝ := min 1 c₀ have hTmin_pos : 0 < Tmin := by dsimp [Tmin]; exact lt_min (by norm_num : (0 : ℝ) < 1) hc₀pos let c : ℝ := Tmin / (2 * (K + M + 1) * (Smax + 1)) have hc_pos : 0 < c := by dsimp [c]; positivity have hc_le_inv : c * (K + M) ≤ 1 := by dsimp [c, Tmin] have hden_pos : 0 < 2 * (K + M + 1) * (Smax + 1) := by positivity rw [div_mul_eq_mul_div, div_le_iff₀ hden_pos] have hTmin_le_one : min 1 c₀ ≤ 1 := min_le_left 1 c₀ have hTmin_nonneg : 0 ≤ min 1 c₀ := le_of_lt hTmin_pos have hSmax : 0 ≤ Smax := le_of_lt hSmax_pos have hKM : 0 ≤ K + M := le_of_lt (add_pos hKpos hMpos) nlinarith have hmain : ∀ n, c * akraBazziScale p g n ≤ T n := by intro n induction n using Nat.strong_induction_on with | h n ih => by_cases hn0 : n = 0 · subst n rw [hsat.1] have hF0 : akraBazziScale p g 0 = 0 := by unfold akraBazziScale akraBazziIntegral have h0pow : (0 : ℝ) ^ p = 0 := Real.zero_rpow (ne_of_gt hp) simp [h0pow] rw [hF0] simp · have hn_pos : 0 < n := Nat.pos_of_ne_zero hn0 have hn_pos' : 1 ≤ n := Nat.succ_le_iff.mpr hn_pos by_cases hle : n ≤ N₀ · have hscale_le_Smax : akraBazziScale p g n ≤ Smax := by dsimp [Smax] have hn_mem : n ∈ Finset.range (N₀ + 1) := by rw [Finset.mem_range] exact Nat.lt_succ_of_le hle exact Finset.single_le_sum (by intro m _hm; exact akraBazziScale_nonneg hp.le hgnonneg m) hn_mem have hT_ge_Tmin : Tmin ≤ T n := by dsimp [Tmin] by_cases hle₀ : n ≤ n₀ · rw [hsat.2.1 n hn_pos' hle₀] exact min_le_left 1 c₀ · have hn₀n : n₀ < n := lt_of_not_ge hle₀ have hg : c₀ * (n : ℝ) ^ p ≤ g n := hglower n hn_pos' have hT_ge_g : g n ≤ T n := akraBazzi_T_ge_g hvalid hgnonneg hsat n hn₀n have hnp : 1 ≤ (n : ℝ) ^ p := by have hn1 : 1 ≤ (n : ℝ) := by exact_mod_cast hn_pos' exact Real.one_le_rpow hn1 hp.le calc min 1 c₀ ≤ c₀ := min_le_right 1 c₀ _ ≤ c₀ * (n : ℝ) ^ p := by nlinarith [hc₀pos, hnp] _ ≤ g n := hg _ ≤ T n := hT_ge_g calc c * akraBazziScale p g n ≤ c * Smax := mul_le_mul_of_nonneg_left hscale_le_Smax hc_pos.le _ ≤ Tmin := by dsimp [c] have hden_pos : 0 < 2 * (K + M + 1) * (Smax + 1) := by positivity rw [div_mul_eq_mul_div, div_le_iff₀ hden_pos] have hSmax_nonneg : 0 ≤ Smax := le_of_lt hSmax_pos have hKM : 0 ≤ K + M := le_of_lt (add_pos hKpos hMpos) have hD_ge_Smax : Smax ≤ 2 * (K + M + 1) * (Smax + 1) := by nlinarith nlinarith [mul_le_mul_of_nonneg_left hD_ge_Smax (le_of_lt hTmin_pos)] _ ≤ T n := hT_ge_Tmin · have hN₀n : N₀ < n := lt_of_not_ge hle have hIH : ∀ ab ∈ branches, c * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊) ≤ T (⌊(n : ℝ) / ab.2⌋₊) := by intro ab hab have hvalid_ab : BranchValid ab := hvalid ab hab have hlt : ⌊(n : ℝ) / ab.2⌋₊ < n := floor_div_lt_self hvalid_ab.2 hn_pos exact ih (⌊(n : ℝ) / ab.2⌋₊) hlt have hchildren : c * (branches.map (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊))).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum := by calc c * (branches.map (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊))).sum = (branches.map (fun ab => (ab.1 : ℝ) * (c * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by rw [show (branches.map (fun ab => (ab.1 : ℝ) * (c * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)))).sum = (branches.map (fun ab => c * ((ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)))).sum by exact congrArg List.sum (List.map_congr_left (by intro ab _hab; ring))] rw [List.sum_map_mul_left branches (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊)) c] _ ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum := by apply List.sum_le_sum intro ab hab have hvalid_ab : BranchValid ab := hvalid ab hab exact mul_le_mul_of_nonneg_left (hIH ab hab) (Nat.cast_nonneg ab.1) have hN₀n' : N₀ ≤ n := le_of_lt hN₀n have hE := hEloss n hN₀n' have hincn : (branches.map (fun ab => akraBazziIncrement p g ab n)).sum ≤ K * g n := by have hn₁ : n₁ ≤ n := le_trans (Nat.le_max_left n₁ n₂) (by omega) exact hinc n hn₁ have hdecomp := akraBazzi_scale_floor_decomp branches p g n hvalid hroot calc c * akraBazziScale p g n = c * ((branches.map (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊))).sum + (branches.map (fun ab => akraBazziIncrement p g ab n)).sum + (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum) := by rw [hdecomp] ring _ = c * (branches.map (fun ab => (ab.1 : ℝ) * akraBazziScale p g (⌊(n : ℝ) / ab.2⌋₊))).sum + c * (branches.map (fun ab => akraBazziIncrement p g ab n)).sum + c * (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum := by ring _ ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum + c * (K * g n) + c * (M * g n) := by have h1 := add_le_add_right hchildren (c * (branches.map (fun ab => akraBazziIncrement p g ab n)).sum + c * (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum) have h2 : c * (branches.map (fun ab => akraBazziIncrement p g ab n)).sum ≤ c * (K * g n) := mul_le_mul_of_nonneg_left hincn hc_pos.le have h3 : c * (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p - (⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziIntegral p g (⌊(n : ℝ) / ab.2⌋₊)))).sum ≤ c * (M * g n) := mul_le_mul_of_nonneg_left hE hc_pos.le linarith _ = (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum + c * (K + M) * g n := by ring _ ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum + g n := by have hg_nonneg : 0 ≤ g n := hgnonneg n have hcm : c * (K + M) ≤ 1 := hc_le_inv nlinarith _ = T n := by have hn₀_le_N₀ : n₀ ≤ N₀ := by omega have hn₀n : n₀ < n := lt_of_le_of_lt hn₀_le_N₀ hN₀n rw [hsat.2.2 n hn₀n] rw [Chapter03.isBigOmega_iff] refine ⟨c, hc_pos, 0, ?_⟩ intro n _hn rw [abs_of_nonneg (akraBazziScale_nonneg hp.le hgnonneg n)] rw [abs_of_nonneg (hT_nonneg n)] exact hmain n

Akra–Bazzi asymptotic bound (critical regime). When the forcing exponent equals the root exponent p, the solution satisfies T(n) = Θ(n^p (1 + Σ_{u≤n} g(u)/u^(p+1))).

theorem akraBazzi_bigTheta_critical {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p : ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches p) (hp : 0 < p) (hsmooth : PolynomialGrowth g p) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigTheta T (akraBazziScale p g) := by constructor · exact akraBazzi_upper_bound hvalid hnonempty hroot hp hp.le hsmooth hsat · exact akraBazzi_lower_bound_critical hvalid hnonempty hroot hp hsmooth hsat

Akra–Bazzi asymptotic bound (forcing-dominated regime). For p + 1 ≤ q the solution satisfies T(n) = Θ(n^p (1 + Σ_{u≤n} g(u)/u^(p+1))).

theorem akraBazzi_bigTheta {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p q : ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches p) (hp : 0 < p) (hpq : p + 1 ≤ q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigTheta T (akraBazziScale p g) := by constructor · exact akraBazzi_upper_bound hvalid hnonempty hroot hp (by linarith [hpq]) hsmooth hsat · exact akraBazzi_lower_bound hvalid hnonempty hroot hp hpq hsmooth hsat

The deep leaf-dominated regime (q < p)

The smoothing function ε x = 1 / √x, used to absorb the constant floor perturbation in the deep leaf-dominated regime q < p. It is nonnegative and strictly decreasing on the positive reals, and its drop ε(x/b) - ε x = (√b - 1) · x^(-1/2) dominates the one-step relative power loss of the floor.

noncomputable def akraBazziSmoothingFn (x : ℝ) : ℝ := (Real.sqrt x)⁻¹

Smoothing gain dominates the one-step floor loss. For b > 1 and p > 0, eventually (n/(2b))^p (√b - 1) / √n ≥ 2(1+p) (n/b)^(p-1) (1 + 1/√n), the comparison that lets the smoothing factor absorb the constant floor loss.

try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead. lemma akraBazzi_smoothing_gain_ge_loss {b p : ℝ} (hb : 1 < b) (hp : 0 < p) : ∃ K : ℝ, 0 < K ∧ ∀ n : ℕ, 1 ≤ n → K ≤ (n : ℝ) ^ (1 / 2 : ℝ) → (n : ℝ) ^ p / (2 * b) ^ p * ((Real.sqrt b - 1) * (Real.sqrt (n : ℝ))⁻¹) ≥ (2 * (1 + p)) * ((n : ℝ) / b) ^ (p - 1) * (1 + (Real.sqrt (n : ℝ))⁻¹) := by have hb_pos : 0 < b := lt_trans (by norm_num : (0 : ℝ) < 1) hb have hb_sqrt_minus_one : 0 < Real.sqrt b - 1 := by have h1 : 1 < Real.sqrt b := by simpa using (Real.sqrt_lt_sqrt (by norm_num : 0 ≤ (1 : ℝ)) hb) linarith let C : ℝ := 2 * (1 + p) have hC_pos : 0 < C := by dsimp [C]; positivity let K : ℝ := 2 * C * (2 : ℝ) ^ p * b / (Real.sqrt b - 1) have hK_pos : 0 < K := by dsimp [K]; positivity refine ⟨K, hK_pos, ?_⟩ intro n hn1 hnK have hn_pos : 0 < (n : ℝ) := by exact_mod_cast (lt_of_lt_of_le (by norm_num : (0 : ℕ) < 1) hn1) have hsqrt_n_pos : 0 < Real.sqrt (n : ℝ) := (Real.sqrt_pos).2 hn_pos have hsqrt_eq : (n : ℝ) ^ (1 / 2 : ℝ) = Real.sqrt (n : ℝ) := (Real.sqrt_eq_rpow (n : ℝ)).symm have hkey : 2 * C * (2 : ℝ) ^ p * b ≤ (Real.sqrt b - 1) * Real.sqrt (n : ℝ) := by rw [hsqrt_eq] at hnK have h := (div_le_iff₀ hb_sqrt_minus_one).mp (by simpa [K] using hnK) nlinarith have hsqrt_ge_one : 1 ≤ Real.sqrt (n : ℝ) := by rw [← Real.sqrt_one] exact Real.sqrt_le_sqrt (by exact_mod_cast hn1) have hfinal : (n : ℝ) * (Real.sqrt b - 1) ≥ C * (2 : ℝ) ^ p * b * (Real.sqrt (n : ℝ) + 1) := by calc (n : ℝ) * (Real.sqrt b - 1) = (Real.sqrt (n : ℝ)) ^ 2 * (Real.sqrt b - 1) := by rw [Real.sq_sqrt (le_of_lt hn_pos)] _ = (Real.sqrt b - 1) * Real.sqrt (n : ℝ) * Real.sqrt (n : ℝ) := by ring _ ≥ (2 * C * (2 : ℝ) ^ p * b) * Real.sqrt (n : ℝ) := by exact mul_le_mul_of_nonneg_right hkey (le_of_lt hsqrt_n_pos) _ = 2 * C * (2 : ℝ) ^ p * b * Real.sqrt (n : ℝ) := by ring _ ≥ C * (2 : ℝ) ^ p * b * (Real.sqrt (n : ℝ) + 1) := by have h2sqrt : Real.sqrt (n : ℝ) + 1 ≤ 2 * Real.sqrt (n : ℝ) := by linarith have h := mul_le_mul_of_nonneg_left h2sqrt (by positivity : 0 ≤ C * (2 : ℝ) ^ p * b) nlinarith have hnp : (n : ℝ) ^ p = (n : ℝ) ^ (p - 1) * (n : ℝ) := by simpa [show p - 1 + 1 = p by ring] using (Real.rpow_add_one (ne_of_gt hn_pos) (p - 1)) have hfinal_np : (n : ℝ) ^ p * (Real.sqrt b - 1) ≥ C * (2 : ℝ) ^ p * b * (n : ℝ) ^ (p - 1) * (Real.sqrt (n : ℝ) + 1) := by have h := mul_le_mul_of_nonneg_right hfinal (Real.rpow_nonneg (le_of_lt hn_pos) (p - 1)) rw [show (n : ℝ) * (Real.sqrt b - 1) * (n : ℝ) ^ (p - 1) = (n : ℝ) ^ p * (Real.sqrt b - 1) by rw [hnp]; ring] at h nlinarith have h2bp : (2 * b) ^ p = (2 : ℝ) ^ p * b ^ p := by rw [Real.mul_rpow (by norm_num : 0 ≤ (2 : ℝ)) (le_of_lt hb_pos)] have hb_p : b ^ p = b * b ^ (p - 1) := by rw [show p = (p - 1) + 1 by ring] rw [Real.rpow_add_one (ne_of_gt hb_pos) (p - 1)] Try this: [apply] ring_nf The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form. Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ring have hden_pos : 0 < (2 * b) ^ p * Real.sqrt (n : ℝ) := mul_pos (Real.rpow_pos_of_pos (by positivity : 0 < (2 : ℝ) * b) p) hsqrt_n_pos calc (n : ℝ) ^ p / (2 * b) ^ p * ((Real.sqrt b - 1) * (Real.sqrt (n : ℝ))⁻¹) = (n : ℝ) ^ p * (Real.sqrt b - 1) / ((2 * b) ^ p * Real.sqrt (n : ℝ)) := by ring _ ≥ (C * (2 : ℝ) ^ p * b * (n : ℝ) ^ (p - 1) * (Real.sqrt (n : ℝ) + 1)) / ((2 * b) ^ p * Real.sqrt (n : ℝ)) := by exact mul_le_mul_of_nonneg_right hfinal_np (inv_nonneg.mpr (le_of_lt hden_pos)) _ = C * ((n : ℝ) / b) ^ (p - 1) * (1 + (Real.sqrt (n : ℝ))⁻¹) := by rw [h2bp, hb_p] rw [Real.div_rpow (le_of_lt hn_pos) (le_of_lt hb_pos) (p - 1)] field_simp [hsqrt_n_pos.ne', hb_pos.ne', (Real.rpow_pos_of_pos (by norm_num : 0 < (2 : ℝ)) p).ne', (Real.rpow_pos_of_pos hb_pos (p - 1)).ne'] _ = (2 * (1 + p)) * ((n : ℝ) / b) ^ (p - 1) * (1 + (Real.sqrt (n : ℝ))⁻¹) := by try 'simp' instead of 'simpa' Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [C]

Floored smoothing scale is a subsolution. For b > 1 and p > 0, eventually ⌊n/b⌋^p (1 + ε⌊n/b⌋) ≥ (n/b)^p (1 + ε n). This is the discrete analogue of the Kuszmaul–Leiserson smoothing step used by mathlib's AkraBazziRecurrence.­isTheta_asympBound: the factor 1 + ε absorbs the constant floor loss so that the homogeneous induction closes to Ω(n^p) exactly (rather than only Ω(n^(p-ε))).

lemma akraBazzi_smoothing_scale_floor_ge {b : ℝ} (hb : 1 < b) {p : ℝ} (hp : 0 < p) : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ((⌊(n : ℝ) / b⌋₊ : ℝ) ^ p) * (1 + akraBazziSmoothingFn (⌊(n : ℝ) / b⌋₊ : ℝ)) ≥ ((n : ℝ) / b) ^ p * (1 + akraBazziSmoothingFn (n : ℝ)) := by have hb_pos : 0 < b := lt_trans (by norm_num : (0 : ℝ) < 1) hb have hb_sqrt_minus_one : 0 < Real.sqrt b - 1 := by have h1 : 1 < Real.sqrt b := by simpa using (Real.sqrt_lt_sqrt (by norm_num : 0 ≤ (1 : ℝ)) hb) linarith let C : ℝ := 2 * (1 + p) have hC_pos : 0 < C := by dsimp [C]; positivity rcases akraBazzi_smoothing_gain_ge_loss hb hp with ⟨K, hK_pos, hK⟩ let N₁ : ℕ := Nat.ceil (K ^ (2 : ℕ)) + 1 have hN₁_gt : K ^ (2 : ℕ) < (N₁ : ℝ) := by have hceil : K ^ (2 : ℕ) ≤ (Nat.ceil (K ^ (2 : ℕ)) : ℝ) := Nat.le_ceil (K ^ (2 : ℕ)) exact lt_of_le_of_lt hceil (by exact_mod_cast (Nat.lt_succ_self (Nat.ceil (K ^ (2 : ℕ))))) let N₂ : ℕ := Nat.ceil (2 * b) + 1 have hN₂_gt : 2 * b < (N₂ : ℝ) := by have hceil : 2 * b ≤ (Nat.ceil (2 * b) : ℝ) := Nat.le_ceil (2 * b) exact lt_of_le_of_lt hceil (by exact_mod_cast (Nat.lt_succ_self (Nat.ceil (2 * b)))) refine ⟨max N₁ N₂, ?_⟩ intro n hn have hnN₁ : N₁ ≤ n := le_trans (Nat.le_max_left _ _) hn have hnN₂ : N₂ ≤ n := le_trans (Nat.le_max_right _ _) hn have hn1_nat : 1 ≤ n := le_trans (by omega : 1 ≤ N₁) hnN₁ have hn1 : 1 ≤ (n : ℝ) := by exact_mod_cast hn1_nat have hn_pos : 0 < (n : ℝ) := by linarith have hKsq_le : K ^ (2 : ℕ) ≤ (n : ℝ) := le_trans (le_of_lt hN₁_gt) (by exact_mod_cast hnN₁) have hnK : K ≤ (n : ℝ) ^ (1 / 2 : ℝ) := by have hsqrt : (n : ℝ) ^ (1 / 2 : ℝ) = Real.sqrt (n : ℝ) := (Real.sqrt_eq_rpow (n : ℝ)).symm rw [hsqrt] exact (Real.le_sqrt (le_of_lt hK_pos) (Nat.cast_nonneg n)).2 hKsq_le have hn2 : 2 * b ≤ (n : ℝ) := le_trans (le_of_lt hN₂_gt) (by exact_mod_cast hnN₂) let x : ℝ := (⌊(n : ℝ) / b⌋₊ : ℝ) have hnb_nonneg : 0 ≤ (n : ℝ) / b := div_nonneg (le_of_lt hn_pos) (le_of_lt hb_pos) have hx_le : x ≤ (n : ℝ) / b := by simpa [x] using (Nat.floor_le hnb_nonneg) have hx_ge : (n : ℝ) / b - 1 ≤ x := by have h := Nat.lt_floor_add_one ((n : ℝ) / b) simpa [x] using (le_of_lt (by linarith [h]) : (n : ℝ) / b - 1 ≤ x) have hx2 : 2 ≤ (n : ℝ) / b := by rw [le_div_iff₀ hb_pos] exact hn2 have hx_pos : 0 < x := by have h1 : 1 ≤ (n : ℝ) / b - 1 := by linarith [hx2] exact lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_trans h1 hx_ge) have hx_ge_half : (n : ℝ) / (2 * b) ≤ x := by have hhalf_le : (n : ℝ) / (2 * b) ≤ (n : ℝ) / b - 1 := by have hdiv : (n : ℝ) / b - (n : ℝ) / (2 * b) = (n : ℝ) / (2 * b) := by field_simp [ne_of_gt (mul_pos (by norm_num : 0 < (2 : ℝ)) hb_pos)] ring have hnb_ge_one : 1 ≤ (n : ℝ) / (2 * b) := by rw [one_le_div (mul_pos (by norm_num : 0 < (2 : ℝ)) hb_pos)] exact hn2 linarith [hdiv, hnb_ge_one] exact le_trans hhalf_le hx_ge have hgain : (Real.sqrt b - 1) * akraBazziSmoothingFn (n : ℝ) ≤ akraBazziSmoothingFn x - akraBazziSmoothingFn (n : ℝ) := by unfold akraBazziSmoothingFn have hsqrt_nb_pos : 0 < Real.sqrt ((n : ℝ) / b) := (Real.sqrt_pos).2 (div_pos hn_pos hb_pos) have hsqrt_nb_inv : (Real.sqrt ((n : ℝ) / b))⁻¹ = Real.sqrt b / Real.sqrt (n : ℝ) := by rw [Real.sqrt_div (le_of_lt hn_pos) b, inv_div] have hsqrt_x_pos : 0 < Real.sqrt x := (Real.sqrt_pos).2 hx_pos have hsqrt_le : Real.sqrt x ≤ Real.sqrt ((n : ℝ) / b) := Real.sqrt_le_sqrt hx_le have hle : (Real.sqrt ((n : ℝ) / b))⁻¹ ≤ (Real.sqrt x)⁻¹ := (inv_le_inv₀ hsqrt_nb_pos hsqrt_x_pos).2 hsqrt_le rw [hsqrt_nb_inv] at hle have hle' : (Real.sqrt b) * (Real.sqrt (n : ℝ))⁻¹ ≤ (Real.sqrt x)⁻¹ := by simpa [div_eq_mul_inv] using hle calc (Real.sqrt b - 1) * (Real.sqrt (n : ℝ))⁻¹ = (Real.sqrt b) * (Real.sqrt (n : ℝ))⁻¹ - (Real.sqrt (n : ℝ))⁻¹ := by ring _ ≤ (Real.sqrt x)⁻¹ - (Real.sqrt (n : ℝ))⁻¹ := sub_le_sub_right hle' _ have hfloor_loss : ((n : ℝ) / b) ^ p - x ^ p ≤ C * ((n : ℝ) / b) ^ (p - 1) := by simpa [x, C] using (rpow_sub_floor_le_of_two_le hp (by simpa using hx2)) have hεn_nonneg : 0 ≤ akraBazziSmoothingFn (n : ℝ) := by unfold akraBazziSmoothingFn exact inv_nonneg.mpr (Real.sqrt_nonneg _) have hgain_ge_loss : ((n : ℝ) / b) ^ p - x ^ p + (((n : ℝ) / b) ^ p - x ^ p) * akraBazziSmoothingFn (n : ℝ) ≤ x ^ p * (akraBazziSmoothingFn x - akraBazziSmoothingFn (n : ℝ)) := by have hgain_lower_raw := hK n hn1_nat hnK have hgain_lower' : (n : ℝ) ^ p / (2 * b) ^ p * ((Real.sqrt b - 1) * akraBazziSmoothingFn (n : ℝ)) ≥ C * ((n : ℝ) / b) ^ (p - 1) * (1 + akraBazziSmoothingFn (n : ℝ)) := by simpa [akraBazziSmoothingFn, C] using hgain_lower_raw have hx_p_ge : (n : ℝ) ^ p / (2 * b) ^ p ≤ x ^ p := by have hhalf_nonneg : 0 ≤ (n : ℝ) / (2 * b) := div_nonneg (le_of_lt hn_pos) (le_of_lt (mul_pos (by norm_num : 0 < (2 : ℝ)) hb_pos)) have hpow : ((n : ℝ) / (2 * b)) ^ p ≤ x ^ p := Real.rpow_le_rpow hhalf_nonneg hx_ge_half hp.le rwa [Real.div_rpow (le_of_lt hn_pos) (le_of_lt (mul_pos (by norm_num : 0 < (2 : ℝ)) hb_pos)) p] at hpow have hgain_nonneg : 0 ≤ (Real.sqrt b - 1) * akraBazziSmoothingFn (n : ℝ) := mul_nonneg (le_of_lt hb_sqrt_minus_one) hεn_nonneg have hgain_lower : x ^ p * ((Real.sqrt b - 1) * akraBazziSmoothingFn (n : ℝ)) ≥ C * ((n : ℝ) / b) ^ (p - 1) * (1 + akraBazziSmoothingFn (n : ℝ)) := by exact le_trans hgain_lower' (mul_le_mul_of_nonneg_right hx_p_ge hgain_nonneg) have hgain_mul : x ^ p * (akraBazziSmoothingFn x - akraBazziSmoothingFn (n : ℝ)) ≥ C * ((n : ℝ) / b) ^ (p - 1) * (1 + akraBazziSmoothingFn (n : ℝ)) := by exact le_trans hgain_lower (mul_le_mul_of_nonneg_left hgain (Real.rpow_nonneg (le_of_lt hx_pos) p)) have hloss_le : ((n : ℝ) / b) ^ p - x ^ p + (((n : ℝ) / b) ^ p - x ^ p) * akraBazziSmoothingFn (n : ℝ) ≤ C * ((n : ℝ) / b) ^ (p - 1) * (1 + akraBazziSmoothingFn (n : ℝ)) := by have h1 : ((n : ℝ) / b) ^ p - x ^ p ≤ C * ((n : ℝ) / b) ^ (p - 1) := hfloor_loss have h2 : (((n : ℝ) / b) ^ p - x ^ p) * akraBazziSmoothingFn (n : ℝ) ≤ (C * ((n : ℝ) / b) ^ (p - 1)) * akraBazziSmoothingFn (n : ℝ) := mul_le_mul_of_nonneg_right h1 hεn_nonneg nlinarith exact le_trans hloss_le hgain_mul calc ((n : ℝ) / b) ^ p * (1 + akraBazziSmoothingFn (n : ℝ)) = x ^ p + x ^ p * akraBazziSmoothingFn (n : ℝ) + (((n : ℝ) / b) ^ p - x ^ p) * (1 + akraBazziSmoothingFn (n : ℝ)) := by ring _ ≤ x ^ p + x ^ p * akraBazziSmoothingFn (n : ℝ) + x ^ p * (akraBazziSmoothingFn x - akraBazziSmoothingFn (n : ℝ)) := by nlinarith [hgain_ge_loss] _ = x ^ p * (1 + akraBazziSmoothingFn x) := by ring

Floored smoothing scale is a subsolution (multi-branch). The single-branch estimate akraBazzi_smoothing_scale_floor_ge holds uniformly across a finite list of branches.

lemma akraBazzi_smoothing_scale_floor_ge_multi {branches : List (ℕ × ℝ)} {p : ℝ} (hvalid : BranchesValid branches) (hp : 0 < p) : ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ ab ∈ branches, ((⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziSmoothingFn (⌊(n : ℝ) / ab.2⌋₊ : ℝ)) ≥ ((n : ℝ) / ab.2) ^ p * (1 + akraBazziSmoothingFn (n : ℝ)) := by classical induction branches with | nil => exact ⟨0, by intro n _hn ab hab; simp at hab⟩ | cons hd tl ih => rcases ih (fun ab hab => hvalid ab (by simp [hab])) with ⟨Ntl, hNtl⟩ rcases akraBazzi_smoothing_scale_floor_ge (hvalid hd (by simp)).2 hp with ⟨Nhd, hNhd⟩ refine ⟨max Nhd Ntl, ?_⟩ intro n hn ab hab rw [List.mem_cons] at hab rcases hab with rfl | habtl · exact hNhd n (le_trans (Nat.le_max_left _ _) hn) · exact hNtl n (le_trans (Nat.le_max_right _ _) hn) ab habtl

Akra–Bazzi lower bound (leaf-dominated regime). When 0 ≤ q < p the solution is T(n) = Ω(n^p (1 + I n)). The leaf term n^p dominates the driving term g = Θ(n^q), and the integral I n is bounded (akraBazziIntegral_bounded_of_lt), so the scale n^p(1 + I n) is Θ(n^p). The induction is closed by the smoothing factor akraBazziSmoothingFn via akraBazzi_smoothing_scale_floor_ge.

theorem akraBazzi_lower_bound_leaf {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p q : ℝ} (hvalid : BranchesValid branches) (Variable name `hnonempty` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches p) (hp : 0 < p) (hpq : q < p) (hq : 0 ≤ q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigOmega T (akraBazziScale p g) := by have hgnonneg : ∀ n, 0 ≤ g n := hsmooth.1 rcases hsmooth.2.2 with ⟨c₀, _C₀, hc₀pos, _hC₀pos, hglower, _hgupper⟩ have hT_nonneg : ∀ n, 0 ≤ T n := akraBazzi_T_nonneg hvalid hgnonneg hsat have hT_ge_g : ∀ n, n₀ < n → g n ≤ T n := akraBazzi_T_ge_g hvalid hgnonneg hsat rcases akraBazziIntegral_bounded_of_lt hsmooth hpq with ⟨Ci, hIbound⟩ have hIbound0 : 0 ≤ Ci := by simpa [akraBazziIntegral] using (hIbound 0) rcases akraBazzi_smoothing_scale_floor_ge_multi hvalid hp with ⟨N, hN⟩ let N₀ : ℕ := max n₀ N + 1 let F : ℕ → ℝ := fun n => (n : ℝ) ^ p * (1 + akraBazziSmoothingFn (n : ℝ)) let Tmin : ℝ := min 1 c₀ have hTmin_pos : 0 < Tmin := lt_min (by norm_num : (0 : ℝ) < 1) hc₀pos let Smax : ℝ := ∑ m ∈ Finset.range (N₀ + 1), F m have hF_nonneg : ∀ m : ℕ, 0 ≤ F m := by intro m have hmp : 0 ≤ (m : ℝ) ^ p := Real.rpow_nonneg (by positivity) p have hε : 0 ≤ akraBazziSmoothingFn (m : ℝ) := by unfold akraBazziSmoothingFn; exact inv_nonneg.mpr (Real.sqrt_nonneg _) exact mul_nonneg hmp (add_nonneg (by norm_num : 0 ≤ (1 : ℝ)) hε) have hSmax_pos : 0 < Smax := by dsimp [Smax] have h1mem : 1 ∈ Finset.range (N₀ + 1) := by rw [Finset.mem_range]; omega have hF1 : 0 < F 1 := by dsimp [F] have h1p : 0 < ((1 : ℕ) : ℝ) ^ p := Real.rpow_pos_of_pos (by norm_num : 0 < ((1 : ℕ) : ℝ)) p have hε1 : 0 ≤ akraBazziSmoothingFn ((1 : ℕ) : ℝ) := by unfold akraBazziSmoothingFn; exact inv_nonneg.mpr (Real.sqrt_nonneg _) have h1plus : 0 < 1 + akraBazziSmoothingFn ((1 : ℕ) : ℝ) := by linarith exact mul_pos h1p h1plus exact Finset.sum_pos' (by intro m _hm; exact hF_nonneg m) ⟨1, h1mem, hF1⟩ let c : ℝ := Tmin / (2 * (Smax + 1)) have hc_pos : 0 < c := by dsimp [c]; positivity have hc_Smax_le_Tmin : c * Smax ≤ Tmin := by dsimp [c] have hden_pos : 0 < 2 * (Smax + 1) := by positivity rw [div_mul_eq_mul_div, div_le_iff₀ hden_pos] have hSmax_le_den : Smax ≤ 2 * (Smax + 1) := by nlinarith nlinarith [mul_le_mul_of_nonneg_left hSmax_le_den (le_of_lt hTmin_pos)] have hmain : ∀ n : ℕ, c * F n ≤ T n := by intro n induction n using Nat.strong_induction_on with | h n ih => by_cases hn0 : n = 0 · subst n rw [hsat.1] dsimp [F] have h0pow : (0 : ℝ) ^ p = 0 := Real.zero_rpow (ne_of_gt hp) simp [h0pow] · have hn_pos : 0 < n := Nat.pos_of_ne_zero hn0 have hn_pos' : 1 ≤ n := Nat.succ_le_iff.mpr hn_pos by_cases hle : n ≤ N₀ · have hF_le_Smax : F n ≤ Smax := by dsimp [Smax] have hn_mem : n ∈ Finset.range (N₀ + 1) := by rw [Finset.mem_range]; exact Nat.lt_succ_of_le hle exact Finset.single_le_sum (by intro m _hm; exact hF_nonneg m) hn_mem have hT_ge_Tmin : Tmin ≤ T n := by dsimp [Tmin] by_cases hle₀ : n ≤ n₀ · rw [hsat.2.1 n hn_pos' hle₀]; exact min_le_left 1 c₀ · have hn₀n : n₀ < n := lt_of_not_ge hle₀ have hg : c₀ * (n : ℝ) ^ q ≤ g n := hglower n hn_pos' have hT_ge_g_n : g n ≤ T n := hT_ge_g n hn₀n have hnq : 1 ≤ (n : ℝ) ^ q := by have hn1 : 1 ≤ (n : ℝ) := by exact_mod_cast hn_pos' exact Real.one_le_rpow hn1 hq calc min 1 c₀ ≤ c₀ := min_le_right 1 c₀ _ ≤ c₀ * (n : ℝ) ^ q := by nlinarith [hc₀pos, hnq] _ ≤ g n := hg _ ≤ T n := hT_ge_g_n calc c * F n ≤ c * Smax := mul_le_mul_of_nonneg_left hF_le_Smax hc_pos.le _ ≤ Tmin := hc_Smax_le_Tmin _ ≤ T n := hT_ge_Tmin · have hN₀n : N₀ < n := lt_of_not_ge hle have hNn : N ≤ n := by have hN₀_ge_N : N ≤ N₀ := by dsimp [N₀] exact Nat.le_trans (Nat.le_max_right n₀ N) (Nat.le_succ (max n₀ N)) exact le_trans hN₀_ge_N (le_of_lt hN₀n) have hIH : ∀ ab ∈ branches, c * F (⌊(n : ℝ) / ab.2⌋₊) ≤ T (⌊(n : ℝ) / ab.2⌋₊) := by intro ab hab have hvalid_ab : BranchValid ab := hvalid ab hab have hlt : ⌊(n : ℝ) / ab.2⌋₊ < n := floor_div_lt_self hvalid_ab.2 hn_pos exact ih (⌊(n : ℝ) / ab.2⌋₊) hlt have hchildren : c * (branches.map (fun ab => (ab.1 : ℝ) * F (⌊(n : ℝ) / ab.2⌋₊))).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum := by calc c * (branches.map (fun ab => (ab.1 : ℝ) * F (⌊(n : ℝ) / ab.2⌋₊))).sum = (branches.map (fun ab => c * ((ab.1 : ℝ) * F (⌊(n : ℝ) / ab.2⌋₊)))).sum := by rw [List.sum_map_mul_left] _ = (branches.map (fun ab => (ab.1 : ℝ) * (c * F (⌊(n : ℝ) / ab.2⌋₊)))).sum := by apply congrArg List.sum apply List.map_congr_left intro ab _hab; ring _ ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum := by apply List.sum_le_sum intro ab hab exact mul_le_mul_of_nonneg_left (hIH ab hab) (Nat.cast_nonneg ab.1) have hsmoothing : ∀ ab ∈ branches, ((⌊(n : ℝ) / ab.2⌋₊ : ℝ) ^ p) * (1 + akraBazziSmoothingFn (⌊(n : ℝ) / ab.2⌋₊ : ℝ)) ≥ ((n : ℝ) / ab.2) ^ p * (1 + akraBazziSmoothingFn (n : ℝ)) := hN n hNn have hchildren' : c * (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p * (1 + akraBazziSmoothingFn (n : ℝ))))).sum ≤ c * (branches.map (fun ab => (ab.1 : ℝ) * F (⌊(n : ℝ) / ab.2⌋₊))).sum := by apply mul_le_mul_of_nonneg_left _ hc_pos.le apply List.sum_le_sum intro ab hab have h : ((n : ℝ) / ab.2) ^ p * (1 + akraBazziSmoothingFn (n : ℝ)) ≤ F (⌊(n : ℝ) / ab.2⌋₊) := by simpa [F] using (hsmoothing ab hab) exact mul_le_mul_of_nonneg_left h (Nat.cast_nonneg ab.1) have hscale_smooth : (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p * (1 + akraBazziSmoothingFn (n : ℝ))))).sum = F n := by have hscale : (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p)).sum = (n : ℝ) ^ p := akraBazzi_root_scale_invariance branches p hvalid hroot n dsimp [F] calc (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p * (1 + akraBazziSmoothingFn (n : ℝ))))).sum = (branches.map (fun ab => ((ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p) * (1 + akraBazziSmoothingFn (n : ℝ)))).sum := by apply congrArg List.sum; apply List.map_congr_left; intro ab _hab; ring _ = (branches.map (fun ab => (ab.1 : ℝ) * ((n : ℝ) / ab.2) ^ p)).sum * (1 + akraBazziSmoothingFn (n : ℝ)) := by rw [List.sum_map_mul_right] _ = (n : ℝ) ^ p * (1 + akraBazziSmoothingFn (n : ℝ)) := by rw [hscale] have hhn₀n : n₀ < n := by have hN₀_ge_n₀ : n₀ ≤ N₀ := by dsimp [N₀] exact Nat.le_trans (Nat.le_max_left n₀ N) (Nat.le_succ (max n₀ N)) exact lt_of_le_of_lt hN₀_ge_n₀ hN₀n calc c * F n = c * (branches.map (fun ab => (ab.1 : ℝ) * (((n : ℝ) / ab.2) ^ p * (1 + akraBazziSmoothingFn (n : ℝ))))).sum := by rw [hscale_smooth] _ ≤ c * (branches.map (fun ab => (ab.1 : ℝ) * F (⌊(n : ℝ) / ab.2⌋₊))).sum := hchildren' _ ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum := hchildren _ ≤ (branches.map (fun ab => (ab.1 : ℝ) * T (⌊(n : ℝ) / ab.2⌋₊))).sum + g n := le_add_of_nonneg_right (hgnonneg n) _ = T n := by rw [hsat.2.2 n hhn₀n] rw [Chapter03.isBigOmega_iff] refine ⟨c / (1 + Ci), ?_, 0, ?_⟩ · positivity · intro n hn rw [abs_of_nonneg (akraBazziScale_nonneg hp.le hgnonneg n)] rw [abs_of_nonneg (hT_nonneg n)] have hscale_le : akraBazziScale p g n ≤ (1 + Ci) * (n : ℝ) ^ p := by unfold akraBazziScale have hI : akraBazziIntegral p g n ≤ Ci := hIbound n have h1 : 1 + akraBazziIntegral p g n ≤ 1 + Ci := by linarith have hnp : 0 ≤ (n : ℝ) ^ p := Real.rpow_nonneg (by positivity) p calc (n : ℝ) ^ p * (1 + akraBazziIntegral p g n) ≤ (n : ℝ) ^ p * (1 + Ci) := mul_le_mul_of_nonneg_left h1 hnp _ = (1 + Ci) * (n : ℝ) ^ p := by ring have hεn_nonneg : 0 ≤ akraBazziSmoothingFn (n : ℝ) := by unfold akraBazziSmoothingFn; exact inv_nonneg.mpr (Real.sqrt_nonneg _) have hnp_le : (n : ℝ) ^ p ≤ F n := by dsimp [F] have hnp_nonneg : 0 ≤ (n : ℝ) ^ p := Real.rpow_nonneg (by positivity) p nlinarith [mul_nonneg hnp_nonneg hεn_nonneg] calc c / (1 + Ci) * akraBazziScale p g n ≤ c / (1 + Ci) * ((1 + Ci) * (n : ℝ) ^ p) := mul_le_mul_of_nonneg_left hscale_le (le_of_lt (div_pos hc_pos (by positivity : 0 < 1 + Ci))) _ = c * (n : ℝ) ^ p := by field_simp [ne_of_gt (by positivity : 0 < 1 + Ci)] _ ≤ c * F n := mul_le_mul_of_nonneg_left hnp_le hc_pos.le _ ≤ T n := hmain n

Akra–Bazzi asymptotic bound (leaf-dominated regime). For 0 ≤ q < p the solution satisfies T(n) = Θ(n^p (1 + Σ_{u≤n} g(u)/u^(p+1))): the upper bound akraBazzi_upper_bound and the leaf lower bound akraBazzi_lower_bound_leaf both apply.

theorem akraBazzi_bigTheta_leaf {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p q : ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches p) (hp : 0 < p) (hpq : q < p) (hq : 0 ≤ q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigTheta T (akraBazziScale p g) := by constructor · exact akraBazzi_upper_bound hvalid hnonempty hroot hp hq hsmooth hsat · exact akraBazzi_lower_bound_leaf hvalid hnonempty hroot hp hpq hq hsmooth hsat
end Chapter04end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_04.Section_04_7_Akra_Bazzi.Generalized

Akra–Bazzi comparison for all nonnegative polynomial forcing exponents

The discrete power-sum estimate closes the forcing interval p < q < p + 1. At characteristic root zero, induction on the integral itself handles the zero input without requiring a positive power. The resulting theorem akraBazzi_bigTheta_nonneg covers every p, q ≥ 0 under PolynomialGrowth and the floor recurrence SatisfiesAkraBazzi.

This retains the explicit monomial sandwich and monotonicity assumptions on forcing. It does not assert the unrestricted perturbation theorem.

open scoped BigOperatorsnamespace CLRS.Chapter04

The positive power sum estimate, including decreasing summands.

lemma akraBazzi_sum_rpow_le {d : ℝ} (hd : 0 < d) (hd1 : d ≤ 1) (n : ℕ) : (∑ u ∈ Finset.range n, ((u + 1 : ℕ) : ℝ) ^ (d - 1)) ≤ (1 + 1 / d) * (n : ℝ) ^ d := by cases n with | zero => simp [Real.zero_rpow hd.ne'] | succ k => have hant : AntitoneOn (fun x : ℝ => x ^ (d - 1)) (Set.Icc 1 (1 + (k : ℝ))) := by intro x hx y hy hxy exact Real.rpow_le_rpow_of_nonpos (by linarith [hx.1]) hxy (by linarith) have hsum := hant.sum_le_integral have hint : (∫ x : ℝ in 1..1 + (k : ℝ), x ^ (d - 1)) = (((k + 1 : ℕ) : ℝ) ^ d - 1) / d := by rw [integral_rpow (Or.inl (by linarith : -1 < d - 1))] simp only [sub_add_cancel, Real.one_rpow, Nat.cast_add, Nat.cast_one] rw [add_comm (1 : ℝ)] rw [hint] at hsum have hshift : (∑ u ∈ Finset.range (k + 1), ((u + 1 : ℕ) : ℝ) ^ (d - 1)) = 1 + ∑ u ∈ Finset.range k, (1 + ((u + 1 : ℕ) : ℝ)) ^ (d - 1) := by rw [Finset.sum_range_succ'] simp only [Nat.cast_add, Nat.cast_one, zero_add, Real.one_rpow] rw [add_comm] congr 1 apply Finset.sum_congr rfl intro u hu congr 1; ring rw [hshift] have hnp : 1 ≤ ((k + 1 : ℕ) : ℝ) ^ d := Real.one_le_rpow (by exact_mod_cast Nat.succ_le_succ (Nat.zero_le k)) hd.le have hdiv : 0 ≤ d⁻¹ := inv_nonneg.mpr hd.le calc 1 + ∑ u ∈ Finset.range k, (1 + ((u + 1 : ℕ) : ℝ)) ^ (d - 1) ≤ 1 + ((((k + 1 : ℕ) : ℝ) ^ d - 1) / d) := add_le_add_right hsum 1 _ ≤ (1 + 1 / d) * ((k + 1 : ℕ) : ℝ) ^ d := by rw [sub_div, div_eq_mul_inv, one_div] nlinarith

The discrete integral has polynomial growth whenever the forcing exponent strictly exceeds the characteristic exponent.

lemma akraBazzi_integral_le_poly_of_lt {p q : ℝ} {g : ℕ → ℝ} (hsmooth : PolynomialGrowth g q) (hpq : p < q) : ∃ C : ℝ, 0 < C ∧ ∀ n, akraBazziIntegral p g n ≤ C * (n : ℝ) ^ (q - p) := by by_cases hlarge : p + 1 ≤ q · exact akraBazzi_integral_le_poly hsmooth hlarge rcases hsmooth.2.2 with ⟨c, Cg, hc, hCg, hlower, hupper⟩ have hd : 0 < q - p := sub_pos.mpr hpq refine ⟨Cg * (1 + 1 / (q - p)), by positivity, ?_⟩ intro n calc akraBazziIntegral p g n ≤ ∑ u ∈ Finset.range n, Cg * ((u + 1 : ℕ) : ℝ) ^ (q - p - 1) := by apply Finset.sum_le_sum intro u hu have hu0 : 0 < ((u + 1 : ℕ) : ℝ) := by positivity calc g (u + 1) / ((u + 1 : ℕ) : ℝ) ^ (p + 1) ≤ (Cg * ((u + 1 : ℕ) : ℝ) ^ q) / ((u + 1 : ℕ) : ℝ) ^ (p + 1) := div_le_div_of_nonneg_right (hupper _ (by omega)) (Real.rpow_nonneg hu0.le _) _ = Cg * ((u + 1 : ℕ) : ℝ) ^ (q - p - 1) := by rw [mul_div_assoc, ← Real.rpow_sub hu0] congr 2; ring _ = Cg * (∑ u ∈ Finset.range n, ((u + 1 : ℕ) : ℝ) ^ (q - p - 1)) := (Finset.mul_sum ..).symm _ ≤ Cg * ((1 + 1 / (q - p)) * (n : ℝ) ^ (q - p)) := mul_le_mul_of_nonneg_left (akraBazzi_sum_rpow_le hd (by linarith) n) hCg.le _ = _ := by ring

Every strictly larger forcing exponent dominates the integral scale.

theorem akraBazzi_lower_bound_of_lt {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p q : ℝ} (hvalid : BranchesValid branches) (_hnonempty : branches ≠ []) (_hroot : IsAkraBazziRoot branches p) (hp : 0 ≤ p) (hpq : p < q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigOmega T (akraBazziScale p g) := by have hgnonneg : ∀ n, 0 ≤ g n := hsmooth.1 rcases hsmooth.2.2 with ⟨c₀, _C, hc₀pos, _hCpos, hglower, _hgupper⟩ rcases akraBazzi_integral_le_poly_of_lt hsmooth hpq with ⟨Ci, _hCipos, hCi⟩ have hT_nonneg : ∀ n, 0 ≤ T n := akraBazzi_T_nonneg hvalid hgnonneg hsat have hT_ge_g : ∀ n, n₀ < n → g n ≤ T n := akraBazzi_T_ge_g hvalid hgnonneg hsat let c : ℝ := c₀ / (1 + Ci) have hc_pos : 0 < c := div_pos hc₀pos (by positivity) rw [Chapter03.isBigOmega_iff] refine ⟨c, hc_pos, n₀ + 1, ?_⟩ intro n hn have hn₀n : n₀ < n := by omega have hn1 : 1 ≤ n := by omega have hg_lower : c₀ * (n : ℝ) ^ q ≤ g n := hglower n hn1 have hF_le : akraBazziScale p g n ≤ (1 + Ci) * (n : ℝ) ^ q := by unfold akraBazziScale have hI : akraBazziIntegral p g n ≤ Ci * (n : ℝ) ^ (q - p) := hCi n have hnp : (n : ℝ) ^ p ≤ (n : ℝ) ^ q := by have hn' : 1 ≤ (n : ℝ) := by exact_mod_cast hn1 exact Real.rpow_le_rpow_of_exponent_le hn' (by linarith [hpq] : p ≤ q) calc (n : ℝ) ^ p * (1 + akraBazziIntegral p g n) ≤ (n : ℝ) ^ p * (1 + Ci * (n : ℝ) ^ (q - p)) := mul_le_mul_of_nonneg_left (by linarith) (Real.rpow_nonneg (by positivity) p) _ = (n : ℝ) ^ p + Ci * ((n : ℝ) ^ p * (n : ℝ) ^ (q - p)) := by ring _ = (n : ℝ) ^ p + Ci * (n : ℝ) ^ q := by have hn_pos : 0 < (n : ℝ) := by exact_mod_cast (lt_of_lt_of_le (by norm_num : (0:ℕ)<1) hn1) rw [show (n : ℝ) ^ p * (n : ℝ) ^ (q - p) = (n : ℝ) ^ q by rw [← Real.rpow_add hn_pos p (q - p)] congr 1; ring] _ ≤ (n : ℝ) ^ q + Ci * (n : ℝ) ^ q := by nlinarith [hnp] _ = (1 + Ci) * (n : ℝ) ^ q := by ring rw [abs_of_nonneg (akraBazziScale_nonneg hp hgnonneg n)] rw [abs_of_nonneg (hT_nonneg n)] calc c * akraBazziScale p g n ≤ c * ((1 + Ci) * (n : ℝ) ^ q) := mul_le_mul_of_nonneg_left hF_le hc_pos.le _ = c₀ * (n : ℝ) ^ q := by dsimp [c] field_simp [ne_of_gt (by positivity : 0 < 1 + Ci)] _ ≤ g n := hg_lower _ ≤ T n := hT_ge_g n hn₀n

At root zero there is no power-rounding loss in the discrete integral.

lemma akraBazzi_integral_children_zero {branches : List (ℕ × ℝ)} {g : ℕ → ℝ} (hvalid : BranchesValid branches) (hroot : IsAkraBazziRoot branches 0) (n : ℕ) : (branches.map (fun ab => (ab.1 : ℝ) * akraBazziIntegral 0 g ⌊(n : ℝ) / ab.2⌋₊)).sum = akraBazziIntegral 0 g n - (branches.map (fun ab => akraBazziIncrement 0 g ab n)).sum := by have hcoeff : (branches.map (fun ab => (ab.1 : ℝ))).sum = 1 := by simpa [IsAkraBazziRoot, charFun, charTerm] using hroot have hd := akraBazzi_scale_decomp branches 0 g n hvalid hroot simp only [akraBazziScale, Real.rpow_zero, one_mul, mul_one, mul_add, List.sum_map_add] at hd rw [hcoeff] at hd linarith

A zero characteristic exponent also admits the lower integral comparison. The induction uses the integral alone because it vanishes at input zero.

theorem akraBazzi_lower_bound_zero {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {q : ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches 0) (hq : 0 ≤ q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigOmega T (akraBazziScale 0 g) := by have hgn := hsmooth.1 have hTn := akraBazzi_T_nonneg hvalid hgn hsat rcases hsmooth.2.2 with ⟨c₀, C₀, hc₀, hC₀, hgl, hgu⟩ rcases akraBazzi_increment_upper hvalid hnonempty (p := 0) (by norm_num) hgn hsmooth.2.1 with ⟨K, hK, N, hinc⟩ let M : ℕ := max n₀ N + 1 let A : ℝ := min 1 c₀ have hA : 0 < A := lt_min (by norm_num) hc₀ have hI : 0 ≤ akraBazziIntegral 0 g M := akraBazziIntegral_nonneg hgn M let c : ℝ := min (A / (akraBazziIntegral 0 g M + 1)) (1 / (K + 1)) have hc : 0 < c := lt_min (div_pos hA (by positivity)) (by positivity) have hcA : c * (akraBazziIntegral 0 g M + 1) ≤ A := by exact (le_div_iff₀ (by positivity)).mp (min_le_left _ _) have hcK : c * K ≤ 1 := by have h : c * (K + 1) ≤ 1 := (le_div_iff₀ (by positivity)).mp (min_le_right _ _) nlinarith have hTpos : ∀ n, 1 ≤ n → A ≤ T n := by intro n hn by_cases hb : n ≤ n₀ · rw [hsat.2.1 n hn hb] exact min_le_left _ _ · have hforce := akraBazzi_T_ge_g hvalid hgn hsat n (by omega) have hpow : 1 ≤ (n : ℝ) ^ q := Real.one_le_rpow (by exact_mod_cast hn) hq have hlo := hgl n hn have hAc : A ≤ c₀ := min_le_right _ _ nlinarith have hmain : ∀ n, c * akraBazziIntegral 0 g n ≤ T n := by intro n induction n using Nat.strong_induction_on with | h n ih => by_cases hz : n = 0 · subst n simp [akraBazziIntegral, hsat.1] have hn : 1 ≤ n := by omega by_cases hsmall : n ≤ M · have hmono := akraBazziIntegral_mono hgn hsmall (p := 0) have hle := mul_le_mul_of_nonneg_left hmono hc.le have hpos := hTpos n hn nlinarith · have hchild : c * (branches.map (fun ab => (ab.1 : ℝ) * akraBazziIntegral 0 g ⌊(n : ℝ) / ab.2⌋₊)).sum ≤ (branches.map (fun ab => (ab.1 : ℝ) * T ⌊(n : ℝ) / ab.2⌋₊)).sum := by rw [← List.sum_map_mul_left] apply List.sum_le_sum intro ab hab have hh := ih ⌊(n : ℝ) / ab.2⌋₊ (floor_div_lt_self (hvalid ab hab).2 (by omega)) calc c * ((ab.1 : ℝ) * akraBazziIntegral 0 g ⌊(n : ℝ) / ab.2⌋₊) = (ab.1 : ℝ) * (c * akraBazziIntegral 0 g ⌊(n : ℝ) / ab.2⌋₊) := by ring _ ≤ _ := mul_le_mul_of_nonneg_left hh (Nat.cast_nonneg _) rw [akraBazzi_integral_children_zero hvalid hroot n] at hchild have hi := hinc n (show N ≤ n by dsimp [M] at hsmall; omega) have hice := mul_le_mul_of_nonneg_left hi hc.le have hgce := mul_le_mul_of_nonneg_right hcK (hgn n) rw [hsat.2.2 n (by dsimp [M] at hsmall; omega)] nlinarith rcases akraBazziIntegral_lower_const (p := 0) hsmooth with ⟨d, hd, hdI⟩ rw [Chapter03.isBigOmega_iff] refine ⟨c * d / (d + 1), by positivity, 1, ?_⟩ intro n hn rw [abs_of_nonneg (akraBazziScale_nonneg (by norm_num) hgn n), abs_of_nonneg (hTn n)] have hIn := hdI n hn have hcompare : d / (d + 1) * (1 + akraBazziIntegral 0 g n) ≤ akraBazziIntegral 0 g n := by rw [div_mul_eq_mul_div, div_le_iff₀ (by positivity)] nlinarith have hm := mul_le_mul_of_nonneg_left hcompare hc.le simp only [akraBazziScale, Real.rpow_zero, one_mul] calc c * d / (d + 1) * (1 + akraBazziIntegral 0 g n) = c * (d / (d + 1) * (1 + akraBazziIntegral 0 g n)) := by ring _ ≤ c * akraBazziIntegral 0 g n := hm _ ≤ T n := hmain n

All nonnegative polynomial forcing exponents satisfy the discrete Akra–Bazzi comparison, including the zero characteristic root.

theorem akraBazzi_bigTheta_nonneg {branches : List (ℕ × ℝ)} {g T : ℕ → ℝ} {n₀ : ℕ} {p q : ℝ} (hvalid : BranchesValid branches) (hnonempty : branches ≠ []) (hroot : IsAkraBazziRoot branches p) (hp : 0 ≤ p) (hq : 0 ≤ q) (hsmooth : PolynomialGrowth g q) (hsat : SatisfiesAkraBazzi branches g T n₀) : Chapter03.isBigTheta T (akraBazziScale p g) := by refine ⟨akraBazzi_upper_bound_nonneg hvalid hnonempty hroot hp hq hsmooth hsat, ?_⟩ rcases eq_or_lt_of_le hp with hp0 | hp0 · subst p exact akraBazzi_lower_bound_zero hvalid hnonempty hroot hq hsmooth hsat rcases lt_trichotomy q p with hlt | heq | hgt · exact akraBazzi_lower_bound_leaf hvalid hnonempty hroot hp0 hlt hq hsmooth hsat · subst q exact akraBazzi_lower_bound_critical hvalid hnonempty hroot hp0 hsmooth hsat · exact akraBazzi_lower_bound_of_lt hvalid hnonempty hroot hp hgt hsmooth hsat
end CLRS.Chapter04

CLRSLean.Chapter_04.Section_04_6_Master_Theorem_All_Input

The real-log comparison scale n^(log_b a). This is the textbook scale used in the standard CLRS statement of the Master theorem: the homogeneous-solution growth rate without floors and ceilings.

For integer exponents it coincides with the ordinary polynomial scale polynomialScale.

noncomputable def realLogScale (a b : ℕ) (n : ℕ) : ℝ := (n : ℝ) ^ (realLogExponent a b)

CLRSLean.FourthEdition.Chapter_04.Section_04_6_Continuous_Master_Theorem

Continuous master theorem, case 1. When the ratio a / b^p > 1 (so p < log_b a, i.e. the forcing n^p is polynomially smaller than the critical n^(log_b a)), the recursion-tree work is Θ(a^k), matching Θ(n^(log_b a)) on the exact power n = b^k.

theorem continuous_master_case1 (a b p : ℕ) (hb : (b : ℝ) ≠ 0) (hr : 1 < continuousRatio a b p) : Chapter03.isBigTheta (continuousWork a b p) (fun k => (a : ℝ) ^ k) := by have hratio : 1 < (a : ℝ) / (b : ℝ) ^ p := by simpa [continuousRatio] using hr have hpow_identity : ∀ k, (b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ k = (a : ℝ) ^ k := by intro k calc (b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ k = (b : ℝ) ^ (p * k) * ((a : ℝ) ^ k / (b : ℝ) ^ (p * k)) := by rw [div_pow, ← pow_mul] _ = (a : ℝ) ^ k := by field_simp [pow_ne_zero (p * k) hb] constructor · rw [Chapter03.isBigO_iff] refine ⟨((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹, inv_pos.mpr (sub_pos.mpr hratio), 0, ?_⟩ intro k hk rw [abs_of_nonneg (continuousWork_nonneg a b p k)] rw [abs_of_nonneg (pow_nonneg (Nat.cast_nonneg a) k)] rw [continuousWork_eq_geomSum a b p hb k] have hgeom : geomSum ((a : ℝ) / (b : ℝ) ^ p) k ≤ ((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * ((a : ℝ) / (b : ℝ) ^ p) ^ k := geomSum_le_geometric_of_gt_one hratio k have hterm : (b : ℝ) ^ (p * k) * geomSum ((a : ℝ) / (b : ℝ) ^ p) k ≤ ((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * (a : ℝ) ^ k := by calc (b : ℝ) ^ (p * k) * geomSum ((a : ℝ) / (b : ℝ) ^ p) k ≤ (b : ℝ) ^ (p * k) * (((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * ((a : ℝ) / (b : ℝ) ^ p) ^ k) := mul_le_mul_of_nonneg_left hgeom (pow_nonneg (Nat.cast_nonneg b) (p * k)) _ = ((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * ((b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ k) := by ring _ = ((a : ℝ) / (b : ℝ) ^ p - 1)⁻¹ * (a : ℝ) ^ k := by rw [hpow_identity k] exact hterm · rw [Chapter03.isBigOmega_iff] refine ⟨((a : ℝ) / (b : ℝ) ^ p)⁻¹, inv_pos.mpr (lt_trans zero_lt_one hratio), 1, ?_⟩ intro k hk rw [abs_of_nonneg (continuousWork_nonneg a b p k)] rw [abs_of_nonneg (pow_nonneg (Nat.cast_nonneg a) k)] rw [continuousWork_eq_geomSum a b p hb k] have hgeom : ((a : ℝ) / (b : ℝ) ^ p)⁻¹ * ((a : ℝ) / (b : ℝ) ^ p) ^ k ≤ geomSum ((a : ℝ) / (b : ℝ) ^ p) k := geometric_le_geomSum_of_gt_one hratio hk have hterm : ((a : ℝ) / (b : ℝ) ^ p)⁻¹ * (a : ℝ) ^ k ≤ (b : ℝ) ^ (p * k) * geomSum ((a : ℝ) / (b : ℝ) ^ p) k := by calc ((a : ℝ) / (b : ℝ) ^ p)⁻¹ * (a : ℝ) ^ k = ((a : ℝ) / (b : ℝ) ^ p)⁻¹ * ((b : ℝ) ^ (p * k) * ((a : ℝ) / (b : ℝ) ^ p) ^ k) := by rw [hpow_identity k] _ = (b : ℝ) ^ (p * k) * (((a : ℝ) / (b : ℝ) ^ p)⁻¹ * ((a : ℝ) / (b : ℝ) ^ p) ^ k) := by ring _ ≤ (b : ℝ) ^ (p * k) * geomSum ((a : ℝ) / (b : ℝ) ^ p) k := mul_le_mul_of_nonneg_left hgeom (pow_nonneg (Nat.cast_nonneg b) (p * k)) exact hterm

Continuous master theorem, case 2. When the ratio a / b^p = 1 (so a = b^p, i.e. the forcing n^p matches the critical n^(log_b a)), the recursion-tree work is Θ(k · a^k), the logarithmic case.

theorem continuous_master_case2 (a b p : ℕ) (hb : (b : ℝ) ≠ 0) (hr : continuousRatio a b p = 1) : Chapter03.isBigTheta (continuousWork a b p) (fun k => (k : ℝ) * (a : ℝ) ^ k) := by have hratio : (a : ℝ) / (b : ℝ) ^ p = 1 := by simpa [continuousRatio] using hr have hbp : (b : ℝ) ^ p ≠ 0 := pow_ne_zero p hb have hbase : (b : ℝ) ^ p = (a : ℝ) := by field_simp [hbp] at hratio exact hratio.symm have hpow_identity : ∀ k, (b : ℝ) ^ (p * k) = (a : ℝ) ^ k := by intro k rw [← hbase] rw [← pow_mul] constructor · rw [Chapter03.isBigO_iff] refine ⟨1, by norm_num, 0, ?_⟩ intro k hk rw [abs_of_nonneg (continuousWork_nonneg a b p k)] rw [abs_of_nonneg (mul_nonneg (Nat.cast_nonneg k) (pow_nonneg (Nat.cast_nonneg a) k))] rw [continuousWork_eq_geomSum a b p hb k] rw [continuousRatio, hratio, geomSum_eq_of_one k] rw [hpow_identity k] nlinarith · rw [Chapter03.isBigOmega_iff] refine ⟨1, by norm_num, 0, ?_⟩ intro k hk rw [abs_of_nonneg (continuousWork_nonneg a b p k)] rw [abs_of_nonneg (mul_nonneg (Nat.cast_nonneg k) (pow_nonneg (Nat.cast_nonneg a) k))] rw [continuousWork_eq_geomSum a b p hb k] rw [continuousRatio, hratio, geomSum_eq_of_one k] rw [hpow_identity k] nlinarith

Continuous master theorem, case 3. When the ratio a / b^p < 1 (so p > log_b a, i.e. the forcing n^p dominates the critical n^(log_b a)), the recursion-tree work is Θ(b^(p·k)), matching Θ(f(n)) = Θ(n^p) on the exact power n = b^k.

theorem continuous_master_case3 (a b p : ℕ) (hb : (b : ℝ) ≠ 0) (hr0 : 0 ≤ continuousRatio a b p) (hr1 : continuousRatio a b p < 1) : Chapter03.isBigTheta (continuousWork a b p) (fun k => (b : ℝ) ^ (p * k)) := by have hratio0 : 0 ≤ (a : ℝ) / (b : ℝ) ^ p := by simpa [continuousRatio] using hr0 have hratio1 : (a : ℝ) / (b : ℝ) ^ p < 1 := by simpa [continuousRatio] using hr1 constructor · rw [Chapter03.isBigO_iff] refine ⟨(1 - (a : ℝ) / (b : ℝ) ^ p)⁻¹, inv_pos.mpr (sub_pos.mpr hratio1), 0, ?_⟩ intro k hk rw [abs_of_nonneg (continuousWork_nonneg a b p k)] rw [abs_of_nonneg (pow_nonneg (Nat.cast_nonneg b) (p * k))] rw [continuousWork_eq_geomSum a b p hb k] rw [continuousRatio] have hgeom : geomSum ((a : ℝ) / (b : ℝ) ^ p) k ≤ (1 - (a : ℝ) / (b : ℝ) ^ p)⁻¹ := geomSum_le_of_lt_one hratio0 hratio1 k have hle := mul_le_mul_of_nonneg_left hgeom (pow_nonneg (Nat.cast_nonneg b) (p * k)) simpa [mul_comm, mul_left_comm, mul_assoc] using hle · rw [Chapter03.isBigOmega_iff] refine ⟨1, by norm_num, 1, ?_⟩ intro k hk have hk1 : 1 ≤ k := hk rw [abs_of_nonneg (continuousWork_nonneg a b p k)] rw [abs_of_nonneg (pow_nonneg (Nat.cast_nonneg b) (p * k))] rw [continuousWork_eq_geomSum a b p hb k] rw [continuousRatio] have hgeom : 1 ≤ geomSum ((a : ℝ) / (b : ℝ) ^ p) k := by rw [geomSum] rw [show (1 : ℝ) = ((a : ℝ) / (b : ℝ) ^ p) ^ 0 by simp] exact Finset.single_le_sum (f := fun j => ((a : ℝ) / (b : ℝ) ^ p) ^ j) (by intro j hj; exact pow_nonneg hratio0 j) (a := 0) (by rw [mem_range]; exact lt_of_lt_of_le zero_lt_one hk1) simpa [mul_comm, mul_left_comm, mul_assoc] using (mul_le_mul_of_nonneg_left hgeom (pow_nonneg (Nat.cast_nonneg b) (p * k)))